1  /-
  2  Copyright (c) 2018 Mario Carneiro. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Mario Carneiro, Sean Leather
  5  
  6  Functions on lists of sigma types.
  7  -/
  8  import data.list.perm data.sigma
src         └────────────┘ └────────┘
  9  
 10  universes u v
 11  
 12  namespace list
 13  variables {α : Type u} {β : α → Type v}
 14  
 15  /- keys -/
 16  
 17  /-- List of keys from a list of key-value pairs -/
 18  def keys : list (sigma β) → list α :=
id              └──┘  └───┘     └──┘ 
src             └──┘  └───┘      └──┘
typ             └──┘  └───┘     └──┘ 
 19  map sigma.fst
id   └─┘ └───────┘
src  └─┘ └───────┘
typ  └─┘ └───────┘
 20  
 21  @[simp] theorem keys_nil : @keys α β [] = [] :=
id                               └──┘   └┘  └┘
src                              └──┘     └┘  └┘
typ                              └──┘   └┘  └┘
doc    └──┘                      └──┘
 22  rfl
id   └─┘
src  └─┘
typ  └─┘
 23  
 24  @[simp] theorem keys_cons {s} {l : list (sigma β)} : (s :: l).keys = s.1 :: l.keys :=
id                                      └──┘  └───┘        └┘  └──┘     └┘ └───┘
src                                     └──┘  └───┘          └┘   └──┘      └┘  └───┘
typ                                     └──┘  └───┘        └┘  └──┘     └┘ └───┘
doc    └──┘                                                       └──┘            └───┘
 25  rfl
id   └─┘
src  └─┘
typ  └─┘
 26  
 27  theorem mem_keys_of_mem {s : sigma β} {l : list (sigma β)} : s ∈ l → s.1 ∈ l.keys :=
id                                └───┘        └──┘  └───┘              └───┘
src                               └───┘         └──┘  └───┘                   └───┘
typ                               └───┘        └──┘  └───┘              └───┘
doc                                                                              └───┘
 28  mem_map_of_mem sigma.fst
id   └────────────┘ └───────┘
src  └────────────┘ └───────┘
typ  └────────────┘ └───────┘
 29  
 30  theorem exists_of_mem_keys {a} {l : list (sigma β)} (h : a ∈ l.keys) :
id                                       └──┘  └───┘           └───┘
src                                      └──┘  └───┘              └───┘
typ                                      └──┘  └───┘           └───┘
doc                                                                └───┘
 31    ∃ (b : β a), sigma.mk a b ∈ l :=
id              └──────┘    
src               └──────┘     
typ             └──────┘    
 32  let ⟨⟨a', b'⟩, m, e⟩ := exists_of_mem_map h in
id   └─┘       └┘          └───────────────┘ 
src                          └───────────────┘
typ  └─┘       └┘          └───────────────┘ 
 33  eq.rec_on e (exists.intro b' m)
id   └───────┘    └──────────┘
src  └───────┘    └──────────┘
typ  └───────┘    └──────────┘
 34  
 35  theorem mem_keys {a} {l : list (sigma β)} : a ∈ l.keys ↔ ∃ (b : β a), sigma.mk a b ∈ l :=
id                             └──┘  └───┘        └───┘           └──────┘    
src                            └──┘  └───┘           └───┘             └──────┘     
typ                            └──┘  └───┘        └───┘           └──────┘    
doc                                                   └───┘
 36  ⟨exists_of_mem_keys, λ ⟨b, h⟩, mem_keys_of_mem h⟩
id    └────────────────┘          └─────────────┘
src   └────────────────┘            └─────────────┘
typ   └────────────────┘          └─────────────┘
 37  
 38  theorem not_mem_keys {a} {l : list (sigma β)} : a ∉ l.keys ↔ ∀ b : β a, sigma.mk a b ∉ l :=
id                                 └──┘  └───┘        └───┘           └──────┘    
src                                └──┘  └───┘           └───┘             └──────┘     
typ                                └──┘  └───┘        └───┘           └──────┘    
doc                                                       └───┘
 39  (not_iff_not_of_iff mem_keys).trans not_exists
id    └────────────────┘ └──────┘ └───┘  └────────┘
src   └────────────────┘ └──────┘ └───┘  └────────┘
typ   └────────────────┘ └──────┘ └───┘  └────────┘
 40  
 41  theorem not_eq_key {a} {l : list (sigma β)} : a ∉ l.keys ↔ ∀ s : sigma β, s ∈ l → a ≠ s.1 :=
id                               └──┘  └───┘        └───┘        └───┘          
src                              └──┘  └───┘           └───┘        └───┘               
typ                              └──┘  └───┘        └───┘        └───┘          
doc                                                     └───┘
 42  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
 43    (λ h₁ s h₂ e, absurd (mem_keys_of_mem h₂) (by rwa e at h₁))
id        └┘  └┘   └────┘  └─────────────┘ └┘          
src                  └────┘  └─────────────┘         └──┘ └────┘
typ       └┘  └┘   └────┘  └─────────────┘ └┘      └──┘└────┘
doc                                                  └──┘ └────┘
txt                                                  └──┘ └────┘
par                                                  └──┘ └────┘
pid                                                      └────┘
st                                                  └──────────┘
 44    (λ f h₁, let ⟨b, h₂⟩ := exists_of_mem_keys h₁ in f _ h₂ rfl)
id         └┘  └─┘     └┘     └────────────────┘ └┘          └─┘
src                            └────────────────┘              └─┘
typ        └┘  └─┘     └┘     └────────────────┘ └┘          └─┘
 45  
 46  /- nodupkeys -/
 47  
 48  def nodupkeys (l : list (sigma β)) : Prop :=
id                      └──┘  └───┘ 
src                     └──┘  └───┘
typ                     └──┘  └───┘ 
 49  l.keys.nodup
id   └───┘└────┘
src   └───┘└────┘
typ  └───┘└────┘
doc   └───┘└────┘
 50  
 51  theorem nodupkeys_iff_pairwise {l} : nodupkeys l ↔
id                                        └───────┘  
src                                       └───────┘   
typ                                       └───────┘  
 52    pairwise (λ s s' : sigma β, s.1 ≠ s'.1) l := pairwise_map _
id     └──────┘           └───┘      └┘       └──────────┘
src    └──────┘           └───┘                  └──────────┘
typ    └──────┘           └───┘      └┘       └──────────┘
doc    └──────┘
 53  
 54  @[simp] theorem nodupkeys_nil : @nodupkeys α β [] := pairwise.nil
id                                    └───────┘   └┘    └──────────┘
src                                   └───────┘     └┘    └──────────┘
typ                                   └───────┘   └┘    └──────────┘
doc    └──┘
 55  
 56  @[simp] theorem nodupkeys_cons {s : sigma β} {l : list (sigma β)} :
id                                       └───┘        └──┘  └───┘ 
src                                      └───┘         └──┘  └───┘
typ                                      └───┘        └──┘  └───┘ 
doc    └──┘
 57    nodupkeys (s::l) ↔ s.1 ∉ l.keys ∧ nodupkeys l :=
id     └───────┘  └┘      └───┘  └───────┘ 
src    └───────┘   └┘         └───┘  └───────┘
typ    └───────┘  └┘      └───┘  └───────┘ 
doc                              └───┘
 58  by simp [keys, nodupkeys]
id            └──┘  └───────┘
src     └────┘└──┘└┘└───────┘└─
typ     └────┘└──┘└┘└───────┘└─
doc     └────┘└──┘└┘         └─
txt     └────┘    └┘         └─
par     └────┘    └┘         └─
pid             └┘         
st     └───────────────────────
 59  
src  
typ  
doc  
txt  
par  
pid  
st   
 60  theorem nodupkeys.eq_of_fst_eq {l : list (sigma β)}
id                                       └──┘  └───┘ 
src                                      └──┘  └───┘
typ                                      └──┘  └───┘ 
 61    (nd : nodupkeys l) {s s' : sigma β} (h : s ∈ l) (h' : s' ∈ l) :
id           └───────┘           └───┘                  └┘  
src          └───────┘            └───┘                        
typ          └───────┘           └───┘                  └┘  
 62    s.1 = s'.1 → s = s' :=
id        └┘      └┘
src                
typ       └┘      └┘
 63  @forall_of_forall_of_pairwise _
id    └──────────────────────────┘
src   └──────────────────────────┘
typ   └──────────────────────────┘
 64    (λ s s' : sigma β, s.1 = s'.1 → s = s')
id               └───┘      └┘      └┘
src              └───┘                
typ              └───┘      └┘      └┘
 65    (λ s s' H h, (H h.symm).symm) _ (λ x h _, rfl)
id         └┘      └───┘ └──┘            └─┘
src                     └───┘ └──┘               └─┘
typ        └┘      └───┘ └──┘            └─┘
 66    ((nodupkeys_iff_pairwise.1 nd).imp (λ s s' h h', (h h').elim)) _ h _ h'
id       └────────────────────┘  └┘ └─┘      └┘  └┘    └┘ └──┘         └┘
src      └────────────────────┘     └─┘                      └──┘
typ      └────────────────────┘  └┘ └─┘      └┘  └┘    └┘ └──┘         └┘
 67  
 68  theorem nodupkeys.eq_of_mk_mem {a : α} {b b' : β a} {l : list (sigma β)}
id                                                         └──┘  └───┘ 
src                                                           └──┘  └───┘
typ                                                        └──┘  └───┘ 
 69    (nd : nodupkeys l) (h : sigma.mk a b ∈ l) (h' : sigma.mk a b' ∈ l) : b = b' :=
id           └───────┘        └──────┘            └──────┘  └┘        └┘
src          └───────┘         └──────┘               └──────┘              
typ          └───────┘        └──────┘            └──────┘  └┘        └┘
 70  by cases nd.eq_of_fst_eq h h' rfl; refl
id            └─────────────┘  └┘ └─┘
src     └────┘└─────────────┘   └─┘  └────
typ     └────┘└─────────────┘└┘└─┘  └────
doc     └────┘                       └────
txt     └────┘                       └────
par     └────┘                       └────
pid                                     
st     └─────────────────────────────────────
 71  
src  
typ  
doc  
txt  
par  
pid  
st   
 72  theorem nodupkeys_singleton (s : sigma β) : nodupkeys [s] := nodup_singleton _
id                                    └───┘     └───────┘     └─────────────┘
src                                   └───┘      └───────┘      └─────────────┘
typ                                   └───┘     └───────┘     └─────────────┘
 73  
 74  theorem nodupkeys_of_sublist {l₁ l₂ : list (sigma β)} (h : l₁ <+ l₂) : nodupkeys l₂ → nodupkeys l₁ :=
id                                         └──┘  └───┘         └┘ └┘ └┘    └───────┘ └┘   └───────┘ └┘
src                                        └──┘  └───┘             └┘       └───────┘      └───────┘
typ                                        └──┘  └───┘         └┘ └┘ └┘    └───────┘ └┘   └───────┘ └┘
 75  nodup_of_sublist (map_sublist_map _ h)
id   └──────────────┘  └─────────────┘   
src  └──────────────┘  └─────────────┘
typ  └──────────────┘  └─────────────┘   
 76  
 77  theorem nodup_of_nodupkeys {l : list (sigma β)} : nodupkeys l → nodup l :=
id                                   └──┘  └───┘      └───────┘    └───┘ 
src                                  └──┘  └───┘       └───────┘     └───┘
typ                                  └──┘  └───┘      └───────┘    └───┘ 
doc                                                                  └───┘
 78  nodup_of_nodup_map _
id   └────────────────┘
src  └────────────────┘
typ  └────────────────┘
 79  
 80  theorem perm_nodupkeys {l₁ l₂ : list (sigma β)} (h : l₁ ~ l₂) : nodupkeys l₁ ↔ nodupkeys l₂ :=
id                                   └──┘  └───┘         └┘  └┘    └───────┘ └┘  └───────┘ └┘
src                                  └──┘  └───┘                    └───────┘     └───────┘
typ                                  └──┘  └───┘         └┘  └┘    └───────┘ └┘  └───────┘ └┘
doc                                                          
 81  perm_nodup $ perm_map _ h
id   └────────┘   └──────┘   
src  └────────┘   └──────┘
typ  └────────┘   └──────┘   
 82  
 83  theorem nodupkeys_join {L : list (list (sigma β))} :
id                               └──┘  └──┘  └───┘ 
src                              └──┘  └──┘  └───┘
typ                              └──┘  └──┘  └───┘ 
 84    nodupkeys (join L) ↔ (∀ l ∈ L, nodupkeys l) ∧ pairwise disjoint (L.map keys) :=
id     └───────┘  └──┘            └───────┘    └──────┘ └──────┘  └──┘ └──┘
src    └───────┘  └──┘              └───────┘     └──────┘ └──────┘   └──┘ └──┘
typ    └───────┘  └──┘            └───────┘    └──────┘ └──────┘  └──┘ └──┘
doc                                                  └──────┘ └──────┘        └──┘
 85  begin
st   └─────
 86    rw [nodupkeys_iff_pairwise, pairwise_join, pairwise_map],
id         └────────────────────┘  └───────────┘  └──────────┘
src    └──┘└────────────────────┘└┘└───────────┘└┘└──────────┘
typ    └──┘└────────────────────┘└┘└───────────┘└┘└──────────┘
doc    └──┘                      └┘             └┘            
txt    └──┘                      └┘             └┘            
par    └──┘                      └┘             └┘            
pid      └┘                      └┘             └┘            
st   ───────────────────────────┘└─────────────┘└────────────┘└──
 87    refine and_congr (ball_congr $ λ l h, by simp [nodupkeys_iff_pairwise]) _,
id            └───────┘  └────────┘                   └────────────────────┘
src    └─────┘└───────┘ └────────┘  └────┘  └────┘└────────────────────┘└─┘
typ    └─────┘└───────┘ └────────┘  └────┘  └────┘└────────────────────┘└─┘
doc    └─────┘                      └────┘  └────┘                      └─┘
txt    └─────┘                      └────┘  └────┘                      └─┘
par    └─────┘                      └────┘  └────┘                      └─┘
pid                                └────┘  └─────┘                      └──┘
st   ─────────────────────────────────────────┘└────────────────────────────┘└─┘└─
 88    apply iff_of_eq, congr', ext l₁ l₂,
id           └───────┘
src    └────┘└───────┘  └────┘  └───────┘
typ    └────┘└───────┘  └────┘  └───────┘
doc    └────┘           └────┘  └───────┘
txt    └────┘           └────┘  └───────┘
par    └────┘           └────┘  └───────┘
pid                               └────┘
st   ────────────────┘└──────┘└─────────┘└─
 89    simp [keys, disjoint_iff_ne]
id           └──┘  └─────────────┘
src    └────┘└──┘└┘└─────────────┘└┘
typ    └────┘└──┘└┘└─────────────┘└┘
doc    └────┘└──┘└┘               └┘
txt    └────┘    └┘               └┘
par    └────┘    └┘               └┘
pid            └┘               
st   ──────────────────────────────┘
 90  end
st   └─┘
 91  
 92  theorem nodup_enum_map_fst (l : list α) : (l.enum.map prod.fst).nodup :=
id                                   └──┘      └───┘└──┘ └──────┘ └───┘
src                                  └──┘        └───┘└──┘ └──────┘ └───┘
typ                                  └──┘      └───┘└──┘ └──────┘ └───┘
doc                                                                 └───┘
 93  by simp [list.nodup_range]
id            └──────────────┘
src     └────┘└──────────────┘└─
typ     └────┘└──────────────┘└─
doc     └────┘                └─
txt     └────┘                └─
par     └────┘                └─
pid                         
st     └────────────────────────
 94  
src  
typ  
doc  
txt  
par  
pid  
st   
 95  variables [decidable_eq α]
id              └──────────┘
src             └──────────┘
typ             └──────────┘
 96  
 97  /- lookup -/
 98  
 99  /-- `lookup a l` is the first value in `l` corresponding to the key `a`,
100    or `none` if no such element exists. -/
101  def lookup (a : α) : list (sigma β) → option (β a)
id                       └──┘  └───┘    └────┘   
src                       └──┘  └───┘      └────┘
typ                      └──┘  └───┘    └────┘   
102  | []             := none
id     └┘                └──┘
src    └┘                └──┘
typ    └┘                └──┘
103  | (⟨a', b⟩ :: l) := if h : a' = a then some (eq.rec_on h b) else lookup l
id       └┘    └┘      └┘               └──┘  └───────┘          └────┘
src             └┘       └┘                └──┘  └───────┘           └────┘
typ      └┘    └┘      └┘               └──┘  └───────┘          └────┘
104  
105  @[simp] theorem lookup_nil (a : α) : lookup a [] = @none (β a) := rfl
id                                       └────┘  └┘   └──┘        └─┘
src                                       └────┘   └┘   └──┘          └─┘
typ                                      └────┘  └┘   └──┘        └─┘
doc    └──┘                               └────┘
st                  
106  
107  @[simp] theorem lookup_cons_eq (l) (a : α) (b : β a) : lookup a (⟨a, b⟩::l) = some b :=
id                                                       └────┘       └┘   └──┘ 
src                                                         └────┘          └┘    └──┘
typ                                                      └────┘       └┘   └──┘ 
doc    └──┘                                                 └────┘
108  dif_pos rfl
id   └─────┘ └─┘
src  └─────┘ └─┘
typ  └─────┘ └─┘
109  
110  @[simp] theorem lookup_cons_ne (l) {a} :
doc    └──┘
111    ∀ s : sigma β, a ≠ s.1 → lookup a (s::l) = lookup a l
id          └───┘         └────┘   └┘   └────┘  
src          └───┘            └────┘     └┘    └────┘
typ         └───┘         └────┘   └┘   └────┘  
doc                             └────┘            └────┘
112  | ⟨a', b⟩ h := dif_neg h.symm
id                 └─────┘  └───┘
src                 └─────┘  └───┘
typ                └─────┘  └───┘
113  
114  theorem lookup_is_some {a : α} : ∀ {l : list (sigma β)},
id                                         └──┘  └───┘ 
src                                          └──┘  └───┘
typ                                        └──┘  └───┘ 
115    (lookup a l).is_some ↔ a ∈ l.keys
id      └────┘   └─────┘     └───┘
src     └────┘     └─────┘       └───┘
typ     └────┘   └─────┘     └───┘
doc     └────┘                     └───┘
116  | []             := by simp
id     └┘
src    └┘                   └───┘
typ    └┘                   └───┘
doc                         └───┘
txt                         └───┘
par                         └───┘
pid                             
st                         └────┘
117  | (⟨a', b⟩ :: l) := begin
id              └┘
src             └┘
typ             └┘
st                       └─────
118    by_cases h : a = a',
id                    └┘
src    └───────┘ └─┘ 
typ    └───────┘ └─┘└┘
doc    └───────┘ └─┘  
txt    └───────┘ └─┘  
par    └───────┘ └─┘  
pid             └─┘  
st   ────────────────────┘└─
119    { subst a', simp },
id             └┘
src      └────┘    └───┘
typ      └────┘└┘  └───┘
doc      └────┘    └───┘
txt      └────┘    └───┘
par      └────┘    └───┘
pid                   
st   ───┘└──────┘└─────┘└┘
120    { simp [h, lookup_is_some] },
id             
src      └────┘ └┘              └┘
typ      └────┘└┘└────────────┘└┘
doc      └────┘ └┘              └┘
txt      └────┘ └┘              └┘
par      └────┘ └┘              └┘
pid           └┘              
st   ────────────────────────────┘└──
121  end
st   ──┘
122  
123  theorem lookup_eq_none {a : α} {l : list (sigma β)} :
id                                      └──┘  └───┘ 
src                                      └──┘  └───┘
typ                                     └──┘  └───┘ 
124    lookup a l = none ↔ a ∉ l.keys :=
id     └────┘    └──┘    └───┘
src    └────┘      └──┘      └───┘
typ    └────┘    └──┘    └───┘
doc    └────┘                   └───┘
125  begin
st   └─────
126    have := not_congr (@lookup_is_some _ _ _ a l),
id             └───────┘   └────────────┘        
src    └──────┘└───────┘  └────────────┘└─────┘  
typ    └──────┘└───────┘  └────────────┘└─────┘
doc    └──────┘                         └─────┘  
txt    └──────┘                         └─────┘  
par    └──────┘                         └─────┘  
pid    └───┘└─┘                         └─────┘  
st   ──────────────────────────────────────────────┘└─
127    simp at this, refine iff.trans _ this,
id                          └───────┘   └──┘
src    └──────────┘  └─────┘└───────┘└─┘
typ    └──────────┘  └─────┘└───────┘└─┘└──┘
doc    └──────────┘  └─────┘         └─┘
txt    └──────────┘  └─────┘         └─┘
par    └──────────┘  └─────┘         └─┘
pid        └─────┘                 └─┘
st   ─────────────┘└───────────────────────┘└─
128    cases lookup a l; exact dec_trivial
id           └────┘          └─────────┘
src    └────┘└────┘    └────┘└─────────┘
typ    └────┘└────┘  └────┘└─────────┘
doc    └────┘└────┘    └────┘└─────────┘
txt    └────┘          └────┘           
par    └────┘          └────┘           
pid                                   
st   ─────────────────────────────────────┘
129  end
st   └─┘
130  
131  theorem of_mem_lookup
132    {a : α} {b : β a} : ∀ {l : list (sigma β)}, b ∈ lookup a l → sigma.mk a b ∈ l
id                            └──┘  └───┘       └────┘     └──────┘    
src                               └──┘  └───┘         └────┘       └──────┘     
typ                           └──┘  └───┘       └────┘     └──────┘    
doc                                                    └────┘
133  | (⟨a', b'⟩ :: l) H := begin
id               └┘
src              └┘
typ              └┘
st                          └─────
134    by_cases h : a = a',
id                    └┘
src    └───────┘ └─┘ 
typ    └───────┘ └─┘└┘
doc    └───────┘ └─┘  
txt    └───────┘ └─┘  
par    └───────┘ └─┘  
pid             └─┘  
st   ────────────────────┘└─
135    { subst a', simp at H, simp [H] },
id             └┘                   
src      └────┘    └───────┘  └────┘ └┘
typ      └────┘└┘  └───────┘  └────┘└┘
doc      └────┘    └───────┘  └────┘ └┘
txt      └────┘    └───────┘  └────┘ └┘
par      └────┘    └───────┘  └────┘ └┘
pid                   └──┘       
st   ───┘└──────┘└─────────┘└─────────┘└┘
136    { simp [h] at H, exact or.inr (of_mem_lookup H) }
id                           └────┘  └───────────┘ 
src      └────┘ └────┘  └────┘└────┘               └┘
typ      └────┘└────┘  └────┘└────┘ └───────────┘└┘
doc      └────┘ └────┘  └────┘                     └┘
txt      └────┘ └────┘  └────┘                     └┘
par      └────┘ └────┘  └────┘                     └┘
pid           └──┘                            
st   ────────────────┘└───────────────────────────────┘└─
137  end
st   ──┘
138  
139  theorem mem_lookup {a} {b : β a} {l : list (sigma β)} (nd : l.nodupkeys)
id                                       └──┘  └───┘          └────────┘
src                                        └──┘  └───┘            └────────┘
typ                                      └──┘  └───┘          └────────┘
140    (h : sigma.mk a b ∈ l) : b ∈ lookup a l :=
id          └──────┘          └────┘  
src         └──────┘              └────┘
typ         └──────┘          └────┘  
doc                                 └────┘
141  begin
st   └─────
142    cases option.is_some_iff_exists.mp (lookup_is_some.mpr (mem_keys_of_mem h)) with b' h',
id           └──────────────────────────┘  └────────────────┘  └─────────────┘ 
src    └────┘└──────────────────────────┘ └────────────────┘ └─────────────┘ └───────────┘
typ    └────┘└──────────────────────────┘ └────────────────┘ └─────────────┘└───────────┘
doc    └────┘                                                                └───────────┘
txt    └────┘                                                                └───────────┘
par    └────┘                                                                └───────────┘
pid                                                                         └┘└─────────┘
st   ───────────────────────────────────────────────────────────────────────────────────────┘└─
143    cases nd.eq_of_mk_mem h (of_mem_lookup h'),
id           └─────────────┘   └───────────┘ └┘
src    └────┘└─────────────┘  └───────────┘  
typ    └────┘└─────────────┘ └───────────┘└┘
doc    └────┘                                
txt    └────┘                                
par    └────┘                                
pid                                         
st   ───────────────────────────────────────────┘└─
144    exact h'
id           └┘
src    └────┘  
typ    └────┘└┘
doc    └────┘  
txt    └────┘  
par    └────┘  
pid           
st   ──────────┘
145  end
st   └─┘
146  
147  theorem map_lookup_eq_find (a : α) : ∀ l : list (sigma β),
id                                            └──┘  └───┘ 
src                                             └──┘  └───┘
typ                                           └──┘  └───┘ 
148    (lookup a l).map (sigma.mk a) = find (λ s, a = s.1) l
id      └────┘   └─┘   └──────┘    └──┘           
src     └────┘     └─┘   └──────┘     └──┘           
typ     └────┘   └─┘   └──────┘    └──┘           
doc     └────┘                         └──┘
149  | [] := rfl
id     └┘    └─┘
src    └┘    └─┘
typ    └┘    └─┘
150  | (⟨a', b'⟩ :: l) := begin
id               └┘
src              └┘
typ              └┘
st                        └─────
151    by_cases h : a = a',
id                    └┘
src    └───────┘ └─┘ 
typ    └───────┘ └─┘└┘
doc    └───────┘ └─┘  
txt    └───────┘ └─┘  
par    └───────┘ └─┘  
pid             └─┘  
st   ────────────────────┘└─
152    { subst a', simp },
id             └┘
src      └────┘    └───┘
typ      └────┘└┘  └───┘
doc      └────┘    └───┘
txt      └────┘    └───┘
par      └────┘    └───┘
pid                   
st   ───┘└──────┘└─────┘└┘
153    { simp [h, map_lookup_eq_find] }
id               └────────────────┘
src      └────┘ └┘                  └┘
typ      └────┘└┘└────────────────┘└┘
doc      └────┘ └┘                  └┘
txt      └────┘ └┘                  └┘
par      └────┘ └┘                  └┘
pid           └┘                  
st   ────────────────────────────────┘└─
154  end
st   ──┘
155  
156  theorem mem_lookup_iff {a : α} {b : β a} {l : list (sigma β)} (nd : l.nodupkeys) :
id                                              └──┘  └───┘          └────────┘
src                                                └──┘  └───┘            └────────┘
typ                                             └──┘  └───┘          └────────┘
157    b ∈ lookup a l ↔ sigma.mk a b ∈ l :=
id       └────┘    └──────┘    
src       └────┘      └──────┘     
typ      └────┘    └──────┘    
doc        └────┘
158  ⟨of_mem_lookup, mem_lookup nd⟩
id    └───────────┘  └────────┘ └┘
src   └───────────┘  └────────┘
typ   └───────────┘  └────────┘ └┘
159  
160  theorem perm_lookup (a : α) {l₁ l₂ : list (sigma β)}
id                                       └──┘  └───┘ 
src                                       └──┘  └───┘
typ                                      └──┘  └───┘ 
161    (nd₁ : l₁.nodupkeys) (nd₂ : l₂.nodupkeys) (p : l₁ ~ l₂) : lookup a l₁ = lookup a l₂ :=
id            └┘└────────┘         └┘└────────┘       └┘  └┘    └────┘  └┘  └────┘  └┘
src             └────────┘           └────────┘                 └────┘       └────┘
typ           └┘└────────┘         └┘└────────┘       └┘  └┘    └────┘  └┘  └────┘  └┘
doc                                                             └────┘        └────┘
162  by ext b; simp [mem_lookup_iff, nd₁, nd₂]; exact mem_of_perm p
id                   └────────────┘  └─┘  └─┘         └─────────┘ 
src     └───┘  └────┘└────────────┘└┘   └┘     └────┘└─────────┘ 
typ     └───┘  └────┘└────────────┘└┘└─┘└┘└─┘  └────┘└─────────┘
doc     └───┘  └────┘              └┘   └┘     └────┘            
txt     └───┘  └────┘              └┘   └┘     └────┘            
par     └───┘  └────┘              └┘   └┘     └────┘            
pid        └┘                    └┘   └┘                      
st     └────────────────────────────────────────────────────────────
163  
src  
typ  
doc  
txt  
par  
pid  
st   
164  lemma mem_ext {l₀ l₁ : list (sigma β)}
id                          └──┘  └───┘ 
src                         └──┘  └───┘
typ                         └──┘  └───┘ 
165    (nd₀ : l₀.nodup) (nd₁ : l₁.nodup)
id            └┘└────┘         └┘└────┘
src             └────┘           └────┘
typ           └┘└────┘         └┘└────┘
doc             └────┘           └────┘
166    (h : ∀ x, x ∈ l₀ ↔ x ∈ l₁) : l₀ ~ l₁ :=
id                └┘    └┘    └┘  └┘
src                                 
typ               └┘    └┘    └┘  └┘
doc                                    
167  begin
st   └─────
168    induction l₀ with x xs generalizing l₁; cases l₁ with x ys,
id               └┘                                  └┘
src    └────────┘  └────────────────────────┘  └────┘  └────────┘
typ    └────────┘└┘└────────────────────────┘  └────┘└┘└────────┘
doc    └────────┘  └────────────────────────┘  └────┘  └────────┘
txt    └────────┘  └────────────────────────┘  └────┘  └────────┘
par    └────────┘  └────────────────────────┘  └────┘  └────────┘
pid               └───────┘└──────────────┘         └────────┘
st   ───────────────────────────────────────────────────────────┘└─
169    { constructor },
src      └──────────┘
typ      └──────────┘
doc      └──────────┘
txt      └──────────┘
par      └──────────┘
pid                 
st   ───┘└──────────┘└┘
170    iterate 2
src    └─────────
typ    └─────────
doc    └─────────
txt    └─────────
par    └─────────
pid           └─
st   ────────────
171    { specialize h x, simp at h,
id                   
src  ───┘└─────────┘  └┘└───────┘└─
typ  ───┘└─────────┘└┘└───────┘└─
doc  ───┘└─────────┘  └┘└───────┘└─
txt  ───┘└─────────┘  └┘└───────┘└─
par  ───┘└─────────┘  └┘└───────┘└─
pid  ──────────────┘  └────────────
st   ─────────────────┘└─────────┘└─
172      cases h },
id             
src  ───┘└────┘ 
typ  ───┘└────┘
doc  ───┘└────┘ 
txt  ───┘└────┘ 
par  ───┘└────┘ 
pid  ─────────┘ └┘
st   ───────────┘└┘
173    simp at nd₀ nd₁, rename x y, classical,
src    └─────────────┘  └────────┘  └───────┘
typ    └─────────────┘  └────────┘  └───────┘
doc    └─────────────┘  └────────┘  └───────┘
txt    └─────────────┘  └────────┘  └───────┘
par    └─────────────┘  └────────┘  └───────┘
pid        └────────┘        └┘└┘
st   ────────────────┘└──────────┘└─────────┘└─
174    cases nd₀, cases nd₁,
id           └─┘        └─┘
src    └────┘     └────┘
typ    └────┘└─┘  └────┘└─┘
doc    └────┘     └────┘
txt    └────┘     └────┘
par    └────┘     └────┘
pid                   
st   ──────────┘└─────────┘└─
175    by_cases h' : x = y,
id                     
src    └───────┘  └─┘ 
typ    └───────┘  └─┘
doc    └───────┘  └─┘  
txt    └───────┘  └─┘  
par    └───────┘  └─┘  
pid              └─┘  
st   ────────────────────┘└─
176    { subst y, constructor, apply l₀_ih ‹ _ › ‹ nodup ys ›,
id                                  └───┘       └───┘ └┘
src      └────┘   └─────────┘  └────┘     └─┘ └───┘  
typ      └────┘  └─────────┘  └────┘└───┘└─┘ └───┘└┘
doc      └────┘   └─────────┘  └────┘     └─┘ └───┘  
txt      └────┘   └─────────┘  └────┘      └─┘         
par      └────┘   └─────────┘  └────┘      └─┘         
pid                                      └─┘         
st   ───┘└─────┘└───────────┘└──────────────────────────────┘└─
177      intro a, specialize h a, simp at h,
id                            
src      └─────┘  └─────────┘    └───────┘
typ      └─────┘  └─────────┘  └───────┘
doc      └─────┘  └─────────┘    └───────┘
txt      └─────┘  └─────────┘    └───────┘
par      └─────┘  └─────────┘    └───────┘
pid           └┘                    └──┘
st   ──────────┘└──────────────┘└─────────┘└─
178      by_cases h' : a = x,
id                        
src      └───────┘  └─┘  
typ      └───────┘  └─┘ 
doc      └───────┘  └─┘  
txt      └───────┘  └─┘  
par      └───────┘  └─┘  
pid                └─┘  
st   ──────────────────────┘└─
179      { subst a, rw ← not_iff_not, split; intro; assumption },
id                      └─────────┘
src        └────┘   └───┘└─────────┘  └───┘  └───┘  └─────────┘
typ        └────┘  └───┘└─────────┘  └───┘  └───┘  └─────────┘
doc        └────┘   └───┘             └───┘  └───┘  └─────────┘
txt        └────┘   └───┘             └───┘  └───┘  └─────────┘
par        └────┘   └───┘             └───┘  └───┘  └─────────┘
pid                  └─┘                                     
st   ─────┘└─────┘└────────────────┘└─────────────────────────┘└┘
180      { simp [h'] at h, exact h } },
id               └┘              
src        └────┘  └────┘  └────┘ 
typ        └────┘└┘└────┘  └────┘
doc        └────┘  └────┘  └────┘ 
txt        └────┘  └────┘  └────┘ 
par        └────┘  └────┘  └────┘ 
pid              └──┘        
st   ───────────────────┘└────────┘└──┘
181    { transitivity x :: y :: ys.erase x,
id                             └──────┘ 
src      └───────────┘      └──────┘
typ      └───────────┘     └──────┘
doc      └───────────┘              
txt      └───────────┘              
par      └───────────┘              
pid                                
st   ────────────────────────────────────┘└─
182      { constructor, apply l₀_ih ‹ _ ›,
id                            └───┘
src        └─────────┘  └────┘      └─┘
typ        └─────────┘  └────┘└───┘ └─┘
doc        └─────────┘  └────┘      └─┘
txt        └─────────┘  └────┘      └─┘
par        └─────────┘  └────┘      └─┘
pid                                └─┘
st   ─────┘└─────────┘└─────────────────┘└─
183        { simp, split, { intro, apply nd₁_left, apply mem_of_mem_erase a },
id                                                       └──────────────┘ 
src          └──┘  └───┘    └───┘  └────┘          └────┘└──────────────┘ 
typ          └──┘  └───┘    └───┘  └────┘          └────┘└──────────────┘
doc          └──┘  └───┘    └───┘  └────┘          └────┘                 
txt          └──┘  └───┘    └───┘  └────┘          └────┘                 
par          └──┘  └───┘    └───┘  └────┘          └────┘                 
pid                                                                     
st   ───────┘└──┘└─────┘└──┘└───┘└──────────────┘└─────────────────────────┘└┘
184          apply nodup_erase_of_nodup; assumption },
id                 └──────────────────┘
src          └────┘└──────────────────┘  └─────────┘
typ          └────┘└──────────────────┘  └─────────┘
doc          └────┘                      └─────────┘
txt          └────┘                      └─────────┘
par          └────┘                      └─────────┘
pid                                               
st   ──────────────────────────────────────────────┘└┘
185        { intro a, specialize h a, simp at h,
id                                
src          └─────┘  └─────────┘    └───────┘
typ          └─────┘  └─────────┘  └───────┘
doc          └─────┘  └─────────┘    └───────┘
txt          └─────┘  └─────────┘    └───────┘
par          └─────┘  └─────────┘    └───────┘
pid               └┘                    └──┘
st   ──────────────┘└──────────────┘└─────────┘└─
186          by_cases h' : a = x,
id                            
src          └───────┘  └─┘  
typ          └───────┘  └─┘ 
doc          └───────┘  └─┘  
txt          └───────┘  └─┘  
par          └───────┘  └─┘  
pid                    └─┘  
st   ──────────────────────────┘└─
187          { subst a, rw ← not_iff_not, split; intro, simp [mem_erase_of_nodup,*], assumption },
id                          └─────────┘                      └────────────────┘
src            └────┘   └───┘└─────────┘  └───┘  └───┘  └────┘└────────────────┘└─┘  └─────────┘
typ            └────┘  └───┘└─────────┘  └───┘  └───┘  └────┘└────────────────┘└─┘  └─────────┘
doc            └────┘   └───┘             └───┘  └───┘  └────┘                  └─┘  └─────────┘
txt            └────┘   └───┘             └───┘  └───┘  └────┘                  └─┘  └─────────┘
par            └────┘   └───┘             └───┘  └───┘  └────┘                  └─┘  └─────────┘
pid                      └─┘                                                 └─┘            
st   ─────────┘└─────┘└────────────────┘└────────────┘└───────────────────────────┘└───────────┘└┘
188          { simp [h'] at h, simp [h], apply or_congr, refl,
id                   └┘                       └──────┘
src            └────┘  └────┘  └────┘   └────┘└──────┘  └──┘
typ            └────┘└┘└────┘  └────┘  └────┘└──────┘  └──┘
doc            └────┘  └────┘  └────┘   └────┘          └──┘
txt            └────┘  └────┘  └────┘   └────┘          └──┘
par            └────┘  └────┘  └────┘   └────┘          └──┘
pid                  └──┘              
st   ───────────────────────┘└────────┘└──────────────┘└────┘└─
189            simp [mem_erase_of_ne,*] } } },
id                   └─────────────┘
src            └────┘└─────────────┘└──┘
typ            └────┘└─────────────┘└──┘
doc            └────┘               └──┘
txt            └────┘               └──┘
par            └────┘               └──┘
pid                               └─┘
st   ──────────────────────────────────┘└────┘
190      transitivity y :: x :: ys.erase x,
id                             └──────┘ 
src      └───────────┘      └──────┘
typ      └───────────┘     └──────┘
doc      └───────────┘              
txt      └───────────┘              
par      └───────────┘              
pid                                
st   ────────────────────────────────────┘└─
191      { constructor },
src        └──────────┘
typ        └──────────┘
doc        └──────────┘
txt        └──────────┘
par        └──────────┘
pid                   
st   ─────┘└──────────┘└┘
192      { constructor, symmetry, apply perm_erase,
id                                      └────────┘
src        └─────────┘  └──────┘  └────┘└────────┘
typ        └─────────┘  └──────┘  └────┘└────────┘
doc        └─────────┘  └──────┘  └────┘
txt        └─────────┘  └──────┘  └────┘
par        └─────────┘  └──────┘  └────┘
pid                                    
st   ────────────────┘└────────┘└────────────────┘└─
193        specialize h x, simp [h'] at h, exact h } }
id                             └┘              
src        └─────────┘    └────┘  └────┘  └────┘ 
typ        └─────────┘  └────┘└┘└────┘  └────┘
doc        └─────────┘    └────┘  └────┘  └────┘ 
txt        └─────────┘    └────┘  └────┘  └────┘ 
par        └─────────┘    └────┘  └────┘  └────┘ 
pid                            └──┘        
st   ───────────────────┘└──────────────┘└────────┘└───
194  end
st   ──┘
195  
196  lemma lookup_ext {l₀ l₁ : list (sigma β)}
id                             └──┘  └───┘ 
src                            └──┘  └───┘
typ                            └──┘  └───┘ 
197    (nd₀ : l₀.nodupkeys) (nd₁ : l₁.nodupkeys)
id            └┘└────────┘         └┘└────────┘
src             └────────┘           └────────┘
typ           └┘└────────┘         └┘└────────┘
198    (h : ∀ x y, y ∈ l₀.lookup x ↔ y ∈ l₁.lookup x) : l₀ ~ l₁ :=
id                 └┘└─────┘     └┘└─────┘     └┘  └┘
src                     └─────┘         └─────┘         
typ                └┘└─────┘     └┘└─────┘     └┘  └┘
doc                      └─────┘           └─────┘         
199  mem_ext (nodup_of_nodupkeys nd₀) (nodup_of_nodupkeys nd₁)
id   └─────┘  └────────────────┘ └─┘   └────────────────┘ └─┘
src  └─────┘  └────────────────┘       └────────────────┘
typ  └─────┘  └────────────────┘ └─┘   └────────────────┘ └─┘
200    (λ ⟨a,b⟩, by rw [← mem_lookup_iff, ← mem_lookup_iff, h]; assumption)
id                       └────────────┘    └────────────┘  
src                 └────┘└────────────┘└──┘└────────────┘└┘   └────────┘
typ                └────┘└────────────┘└──┘└────────────┘└┘  └────────┘
doc                 └────┘              └──┘              └┘   └────────┘
txt                 └────┘              └──┘              └┘   └────────┘
par                 └────┘              └──┘              └┘   └────────┘
pid                   └──┘              └──┘              └┘ 
st                 └───────────────────┘└────────────────┘└─┘└──────────┘
201  
202  /- lookup_all -/
203  
204  /-- `lookup_all a l` is the list of all values in `l` corresponding to the key `a`. -/
205  def lookup_all (a : α) : list (sigma β) → list (β a)
id                           └──┘  └───┘    └──┘   
src                           └──┘  └───┘      └──┘
typ                          └──┘  └───┘    └──┘   
206  | []             := []
id     └┘                └┘
src    └┘                └┘
typ    └┘                └┘
207  | (⟨a', b⟩ :: l) := if h : a' = a then eq.rec_on h b :: lookup_all l else lookup_all l
id       └┘    └┘      └┘               └───────┘    └┘ └────────┘        └────────┘
src             └┘       └┘                └───────┘     └┘
typ      └┘    └┘      └┘               └───────┘    └┘ └────────┘        └────────┘
208  
209  @[simp] theorem lookup_all_nil (a : α) : lookup_all a [] = @nil (β a) := rfl
id                                           └────────┘  └┘   └─┘        └─┘
src                                           └────────┘   └┘   └─┘          └─┘
typ                                          └────────┘  └┘   └─┘        └─┘
doc    └──┘                                   └────────┘
210  
211  @[simp] theorem lookup_all_cons_eq (l) (a : α) (b : β a) :
id                                                       
typ                                                      
doc    └──┘
212    lookup_all a (⟨a, b⟩::l) = b :: lookup_all a l :=
id     └────────┘       └┘    └┘ └────────┘  
src    └────────┘          └┘      └┘ └────────┘
typ    └────────┘       └┘    └┘ └────────┘  
doc    └────────┘                      └────────┘
213  dif_pos rfl
id   └─────┘ └─┘
src  └─────┘ └─┘
typ  └─────┘ └─┘
214  
215  @[simp] theorem lookup_all_cons_ne (l) {a} :
doc    └──┘
216    ∀ s : sigma β, a ≠ s.1 → lookup_all a (s::l) = lookup_all a l
id          └───┘         └────────┘   └┘   └────────┘  
src          └───┘            └────────┘     └┘    └────────┘
typ         └───┘         └────────┘   └┘   └────────┘  
doc                             └────────┘            └────────┘
217  | ⟨a', b⟩ h := dif_neg h.symm
id                 └─────┘  └───┘
src                 └─────┘  └───┘
typ                └─────┘  └───┘
218  
219  theorem lookup_all_eq_nil {a : α} : ∀ {l : list (sigma β)},
id                                            └──┘  └───┘ 
src                                             └──┘  └───┘
typ                                           └──┘  └───┘ 
220    lookup_all a l = [] ↔ ∀ b : β a, sigma.mk a b ∉ l
id     └────────┘    └┘           └──────┘    
src    └────────┘      └┘             └──────┘     
typ    └────────┘    └┘           └──────┘    
doc    └────────┘
221  | []             := by simp
id     └┘
src    └┘                   └───┘
typ    └┘                   └───┘
doc                         └───┘
txt                         └───┘
par                         └───┘
pid                             
st                         └────┘
222  | (⟨a', b⟩ :: l) := begin
id              └┘
src             └┘
typ             └┘
st                       └─────
223    by_cases h : a = a',
id                    └┘
src    └───────┘ └─┘ 
typ    └───────┘ └─┘└┘
doc    └───────┘ └─┘  
txt    └───────┘ └─┘  
par    └───────┘ └─┘  
pid             └─┘  
st   ────────────────────┘└─
224    { subst a', simp, exact λ H, H b (or.inl rfl) },
id             └┘                       └────┘ └─┘
src      └────┘    └──┘  └────┘ └──┘   └────┘└─┘└┘
typ      └────┘└┘  └──┘  └────┘ └──┘  └────┘└─┘└┘
doc      └────┘    └──┘  └────┘ └──┘            └┘
txt      └────┘    └──┘  └────┘ └──┘            └┘
par      └────┘    └──┘  └────┘ └──┘            └┘
pid                           └──┘            
st   ───┘└──────┘└────┘└────────────────────────────┘└┘
225    { simp [h, lookup_all_eq_nil] },
id             
src      └────┘ └┘                 └┘
typ      └────┘└┘└───────────────┘└┘
doc      └────┘ └┘                 └┘
txt      └────┘ └┘                 └┘
par      └────┘ └┘                 └┘
pid           └┘                 
st   ───────────────────────────────┘└──
226  end
st   ──┘
227  
228  theorem head_lookup_all (a : α) : ∀ l : list (sigma β),
id                                         └──┘  └───┘ 
src                                          └──┘  └───┘
typ                                        └──┘  └───┘ 
229    head' (lookup_all a l) = lookup a l
id     └───┘  └────────┘     └────┘  
src    └───┘  └────────┘       └────┘
typ    └───┘  └────────┘     └────┘  
doc           └────────┘        └────┘
230  | []             := by simp
id     └┘
src    └┘                   └───┘
typ    └┘                   └───┘
doc                         └───┘
txt                         └───┘
par                         └───┘
pid                             
st                         └────┘
231  | (⟨a', b⟩ :: l) := by by_cases h : a = a'; [{subst h, simp}, simp *]
id              └┘                         └┘         
src             └┘          └───────┘ └─┘      └────┘   └──┘   └────┘
typ             └┘          └───────┘ └─┘└┘   └────┘  └──┘   └────┘
doc                         └───────┘ └─┘        └────┘   └──┘   └────┘
txt                         └───────┘ └─┘        └────┘   └──┘   └────┘
par                         └───────┘ └─┘        └────┘   └──┘   └────┘
pid                                  └─┘                           
st                         └─────────────────────┘└──────┘└────┘└┘└──────┘
232  
233  theorem mem_lookup_all {a : α} {b : β a} :
id                                       
typ                                      
234    ∀ {l : list (sigma β)}, b ∈ lookup_all a l ↔ sigma.mk a b ∈ l
id           └──┘  └───┘       └────────┘    └──────┘    
src           └──┘  └───┘         └────────┘      └──────┘     
typ          └──┘  └───┘       └────────┘    └──────┘    
doc                                └────────┘
235  | []              := by simp
id     └┘
src    └┘                    └───┘
typ    └┘                    └───┘
doc                          └───┘
txt                          └───┘
par                          └───┘
pid                              
st                          └────┘
236  | (⟨a', b'⟩ :: l) := by by_cases h : a = a'; [{subst h, simp *}, simp *]
id               └┘                         └┘         
src              └┘          └───────┘ └─┘      └────┘   └────┘   └────┘
typ              └┘          └───────┘ └─┘└┘   └────┘  └────┘   └────┘
doc                          └───────┘ └─┘        └────┘   └────┘   └────┘
txt                          └───────┘ └─┘        └────┘   └────┘   └────┘
par                          └───────┘ └─┘        └────┘   └────┘   └────┘
pid                                   └─┘                           
st                          └─────────────────────┘└──────┘└──────┘└┘└──────┘
237  
238  theorem lookup_all_sublist (a : α) :
id                                   
typ                                  
239    ∀ l : list (sigma β), (lookup_all a l).map (sigma.mk a) <+ l
id          └──┘  └───┘     └────────┘   └─┘   └──────┘   └┘ 
src          └──┘  └───┘      └────────┘     └─┘   └──────┘    └┘
typ         └──┘  └───┘     └────────┘   └─┘   └──────┘   └┘ 
doc                           └────────┘
240  | []              := by simp
id     └┘
src    └┘                    └───┘
typ    └┘                    └───┘
doc                          └───┘
txt                          └───┘
par                          └───┘
pid                              
st                          └────┘
241  | (⟨a', b'⟩ :: l) := begin
id               └┘
src              └┘
typ              └┘
st                        └─────
242      by_cases h : a = a',
id                      └┘
src      └───────┘ └─┘ 
typ      └───────┘ └─┘└┘
doc      └───────┘ └─┘  
txt      └───────┘ └─┘  
par      └───────┘ └─┘  
pid               └─┘  
st   ──────────────────────┘└─
243      { subst h, simp, exact (lookup_all_sublist l).cons2 _ _ _ },
id                              └────────────────┘ 
src        └────┘   └──┘  └────┘                    └────────────┘
typ        └────┘  └──┘  └────┘ └────────────────┘└────────────┘
doc        └────┘   └──┘  └────┘                    └────────────┘
txt        └────┘   └──┘  └────┘                    └────────────┘
par        └────┘   └──┘  └────┘                    └────────────┘
pid                                               └───────────┘
st   ─────┘└─────┘└────┘└─────────────────────────────────────────┘└┘
244      { simp [h], exact (lookup_all_sublist l).cons _ _ _ }
id                         └────────────────┘ 
src        └────┘   └────┘                    └───────────┘
typ        └────┘  └────┘ └────────────────┘└───────────┘
doc        └────┘   └────┘                    └───────────┘
txt        └────┘   └────┘                    └───────────┘
par        └────┘   └────┘                    └───────────┘
pid                                        └──────────┘
st   ─────────────┘└────────────────────────────────────────┘└─
245    end
st   ────┘
246  
247  theorem lookup_all_length_le_one (a : α) {l : list (sigma β)} (h : l.nodupkeys) :
id                                                └──┘  └───┘         └────────┘
src                                                └──┘  └───┘           └────────┘
typ                                               └──┘  └───┘         └────────┘
248    length (lookup_all a l) ≤ 1 :=
id     └────┘  └────────┘    
src    └────┘  └────────┘      
typ    └────┘  └────────┘    
doc            └────────┘
249  by have := nodup_of_sublist (map_sublist_map _ $ lookup_all_sublist a l) h;
id              └──────────────┘  └─────────────┘     └────────────────┘    
src     └──────┘└──────────────┘ └─────────────┘└─┘ └────────────────┘  └┘
typ     └──────┘└──────────────┘ └─────────────┘└─┘ └────────────────┘└┘
doc     └──────┘                                └─┘                     └┘
txt     └──────┘                                └─┘                     └┘
par     └──────┘                                └─┘                     └┘
pid     └───┘└─┘                                └─┘                     └┘
st     └─────────────────────────────────────────────────────────────────────────
250     rw map_map at this; rwa [← nodup_repeat, ← map_const _ a]
id         └─────┘                 └──────────┘    └───────┘   
src     └─┘└─────┘└──────┘  └─────┘└──────────┘└──┘└───────┘└─┘ └─
typ     └─┘└─────┘└──────┘  └─────┘└──────────┘└──┘└───────┘└─┘└─
doc     └─┘       └──────┘  └─────┘            └──┘         └─┘ └─
txt     └─┘       └──────┘  └─────┘            └──┘         └─┘ └─
par     └─┘       └──────┘  └─────┘            └──┘         └─┘ └─
pid              └──────┘     └──┘            └──┘         └─┘ 
st   ─────┘└─────┘└─────────────┘└────────────┘└───────────────┘
251  
src  
typ  
doc  
txt  
par  
pid  
st   
252  theorem lookup_all_eq_lookup (a : α) {l : list (sigma β)} (h : l.nodupkeys) :
id                                            └──┘  └───┘         └────────┘
src                                            └──┘  └───┘           └────────┘
typ                                           └──┘  └───┘         └────────┘
253    lookup_all a l = (lookup a l).to_list :=
id     └────────┘     └────┘   └─────┘
src    └────────┘       └────┘     └─────┘
typ    └────────┘     └────┘   └─────┘
doc    └────────┘        └────┘
254  begin
st   └─────
255    rw ← head_lookup_all,
id          └─────────────┘
src    └───┘└─────────────┘
typ    └───┘└─────────────┘
doc    └───┘
txt    └───┘
par    └───┘
pid      └─┘
st   ─────────────────────┘└─
256    have := lookup_all_length_le_one a h, revert this,
id             └──────────────────────┘  
src    └──────┘└──────────────────────┘    └─────────┘
typ    └──────┘└──────────────────────┘  └─────────┘
doc    └──────┘                            └─────────┘
txt    └──────┘                            └─────────┘
par    └──────┘                            └─────────┘
pid    └───┘└─┘                                  └───┘
st   ─────────────────────────────────────┘└───────────┘└─
257    rcases lookup_all a l with _|⟨b, _|⟨c, l⟩⟩; intro; try {refl},
id            └────────┘  
src    └─────┘└────────┘  └───────────────────┘  └───┘  └───┘└──┘
typ    └─────┘└────────┘└───────────────────┘  └───┘  └───┘└──┘
doc    └─────┘└────────┘  └───────────────────┘  └───┘  └───┘└──┘
txt    └─────┘            └───────────────────┘  └───┘  └───┘└──┘
par    └─────┘            └───────────────────┘  └───┘  └───┘└──┘
pid                      └───────────────────┘            └─────┘
st   ─────────────────────────────────────────────────────────┘└──┘└┘
258    exact absurd this dec_trivial
id           └────┘ └──┘ └─────────┘
src    └────┘└────┘    └─────────┘
typ    └────┘└────┘└──┘└─────────┘
doc    └────┘          └─────────┘
txt    └────┘                     
par    └────┘                     
pid                              
st   ───────────────────────────────┘
259  end
st   └─┘
260  
261  theorem lookup_all_nodup (a : α) {l : list (sigma β)} (h : l.nodupkeys) :
id                                        └──┘  └───┘         └────────┘
src                                        └──┘  └───┘           └────────┘
typ                                       └──┘  └───┘         └────────┘
262    (lookup_all a l).nodup :=
id      └────────┘   └───┘
src     └────────┘     └───┘
typ     └────────┘   └───┘
doc     └────────┘     └───┘
263  by rw lookup_all_eq_lookup a h; apply option.to_list_nodup
id         └──────────────────┘          └──────────────────┘
src     └─┘└──────────────────┘    └────┘└──────────────────┘
typ     └─┘└──────────────────┘  └────┘└──────────────────┘
doc     └─┘                        └────┘                    
txt     └─┘                        └────┘                    
par     └─┘                        └────┘                    
pid                                                        
st     └────────────────────────────────────────────────────────
264  
src  
typ  
doc  
txt  
par  
pid  
st   
265  theorem perm_lookup_all (a : α) {l₁ l₂ : list (sigma β)}
id                                           └──┘  └───┘ 
src                                           └──┘  └───┘
typ                                          └──┘  └───┘ 
266    (nd₁ : l₁.nodupkeys) (nd₂ : l₂.nodupkeys) (p : l₁ ~ l₂) : lookup_all a l₁ = lookup_all a l₂ :=
id            └┘└────────┘         └┘└────────┘       └┘  └┘    └────────┘  └┘  └────────┘  └┘
src             └────────┘           └────────┘                 └────────┘       └────────┘
typ           └┘└────────┘         └┘└────────┘       └┘  └┘    └────────┘  └┘  └────────┘  └┘
doc                                                             └────────┘        └────────┘
267  by simp [lookup_all_eq_lookup, nd₁, nd₂, perm_lookup a nd₁ nd₂ p]
id            └──────────────────┘  └─┘  └─┘  └─────────┘  └─┘ └─┘ 
src     └────┘└──────────────────┘└┘   └┘   └┘└─────────┘        └─
typ     └────┘└──────────────────┘└┘└─┘└┘└─┘└┘└─────────┘└─┘└─┘└─
doc     └────┘                    └┘   └┘   └┘                   └─
txt     └────┘                    └┘   └┘   └┘                   └─
par     └────┘                    └┘   └┘   └┘                   └─
pid                             └┘   └┘   └┘                   
st     └───────────────────────────────────────────────────────────────
268  
src  
typ  
doc  
txt  
par  
pid  
st   
269  /- kreplace -/
src  ───────────────
typ  ───────────────
doc  ───────────────
txt  ───────────────
par  ───────────────
pid  ───────────────
st   ───────────────
270  
src  
typ  
doc  
txt  
par  
pid  
st   
271  def kreplace (a : α) (b : β a) : list (sigma β) → list (sigma β) :=
id                                 └──┘  └───┘     └──┘  └───┘ 
src                                   └──┘  └───┘      └──┘  └───┘
typ                                └──┘  └───┘     └──┘  └───┘ 
272  lookmap $ λ s, if h : a = s.1 then some ⟨a, b⟩ else none
id   └─────┘       └┘              └──┘           └──┘
src  └─────┘        └┘                └──┘             └──┘
typ  └─────┘       └┘              └──┘           └──┘
doc  └─────┘
273  
274  theorem kreplace_of_forall_not (a : α) (b : β a) {l : list (sigma β)}
id                                                      └──┘  └───┘ 
src                                                        └──┘  └───┘
typ                                                     └──┘  └───┘ 
275    (H : ∀ b : β a, sigma.mk a b ∉ l) : kreplace a b l = l :=
id                   └──────┘        └──────┘     
src                    └──────┘           └──────┘       
typ                  └──────┘        └──────┘     
276  lookmap_of_forall_not _ $ begin
id   └───────────────────┘
src  └───────────────────┘
typ  └───────────────────┘
st                             └─────
277    rintro ⟨a', b'⟩ h, dsimp, split_ifs,
src    └───────────────┘  └───┘  └───────┘
typ    └───────────────┘  └───┘  └───────┘
doc    └───────────────┘  └───┘  └───────┘
txt    └───────────────┘  └───┘  └───────┘
par    └───────────────┘  └───┘  └───────┘
pid          └─────────┘
st   ──────────────────┘└─────┘└─────────┘└─
278    { subst a', exact H _ h }, {refl}
id             └┘           
src      └────┘    └────┘ └─┘     └──┘
typ      └────┘└┘  └────┘└─┘    └──┘
doc      └────┘    └────┘ └─┘     └──┘
txt      └────┘    └────┘ └─┘     └──┘
par      └────┘    └────┘ └─┘     └──┘
pid                     └─┘ 
st   ───┘└──────┘└────────────┘└┘└────┘└─
279  end
st   ──┘
280  
281  theorem kreplace_self {a : α} {b : β a} {l : list (sigma β)}
id                                             └──┘  └───┘ 
src                                               └──┘  └───┘
typ                                            └──┘  └───┘ 
282    (nd : nodupkeys l) (h : sigma.mk a b ∈ l) : kreplace a b l = l :=
id           └───────┘        └──────┘        └──────┘     
src          └───────┘         └──────┘           └──────┘       
typ          └───────┘        └──────┘        └──────┘     
283  begin
st   └─────
284    refine (lookmap_congr _).trans
id             └───────────┘
src    └─────┘ └───────────┘└─────────
typ    └─────┘ └───────────┘└─────────
doc    └─────┘              └─────────
txt    └─────┘              └─────────
par    └─────┘              └─────────
pid                        └─────────
st   ─────────────────────────────────
285      (lookmap_id' (option.guard (λ s, a = s.1)) _ _),
id        └─────────┘  └──────────┘        
src  ───┘ └─────────┘ └──────────┘  └──┘  └───────┘
typ  ───┘ └─────────┘ └──────────┘  └──┘ └───────┘
doc  ───┘             └──────────┘  └──┘   └───────┘
txt  ───┘                           └──┘   └───────┘
par  ───┘                           └──┘   └───────┘
pid  ───┘                           └──┘   └───────┘
st   ──────────────────────────────────────────────────┘└─
286    { rintro ⟨a', b'⟩ h', dsimp [option.guard], split_ifs,
id                                  └──────────┘
src      └────────────────┘  └─────┘└──────────┘  └───────┘
typ      └────────────────┘  └─────┘└──────────┘  └───────┘
doc      └────────────────┘  └─────┘└──────────┘  └───────┘
txt      └────────────────┘  └─────┘              └───────┘
par      └────────────────┘  └─────┘              └───────┘
pid            └──────────┘                   
st   ───┘└────────────────┘└────────────────────┘└─────────┘└─
287      { subst a', exact ⟨rfl, heq_of_eq $ nd.eq_of_mk_mem h h'⟩ },
id               └┘         └─┘  └───────┘   └─────────────┘  └┘
src        └────┘    └────┘ └─┘└┘└───────┘ └─────────────┘   └┘
typ        └────┘└┘  └────┘ └─┘└┘└───────┘ └─────────────┘└┘└┘
doc        └────┘    └────┘    └┘                            └┘
txt        └────┘    └────┘    └┘                            └┘
par        └────┘    └────┘    └┘                            └┘
pid                          └┘                            
st   ─────┘└──────┘└──────────────────────────────────────────────┘└┘
288      { refl } },
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid            
st   ──────────┘└──┘
289    { rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩, dsimp [option.guard], split_ifs,
id                                        └──────────┘
src      └──────────────────────┘  └─────┘└──────────┘  └───────┘
typ      └──────────────────────┘  └─────┘└──────────┘  └───────┘
doc      └──────────────────────┘  └─────┘└──────────┘  └───────┘
txt      └──────────────────────┘  └─────┘              └───────┘
par      └──────────────────────┘  └─────┘              └───────┘
pid            └────────────────┘                   
st   ───────────────────────────┘└────────────────────┘└─────────┘└─
290      { subst a₁, rintro ⟨⟩, simp }, { rintro ⟨⟩ } },
id               └┘
src        └────┘    └───────┘  └───┘     └────────┘
typ        └────┘└┘  └───────┘  └───┘     └────────┘
doc        └────┘    └───────┘  └───┘     └────────┘
txt        └────┘    └───────┘  └───┘     └────────┘
par        └────┘    └───────┘  └───┘     └────────┘
pid                       └─┘                 └─┘
st   ─────┘└──────┘└─────────┘└─────┘└┘└───────────┘└────
291  end
st   ──┘
292  
293  theorem keys_kreplace (a : α) (b : β a) : ∀ l : list (sigma β),
id                                                └──┘  └───┘ 
src                                                  └──┘  └───┘
typ                                               └──┘  └───┘ 
294    (kreplace a b l).keys = l.keys :=
id      └──────┘    └──┘   └───┘
src     └──────┘       └──┘    └───┘
typ     └──────┘    └──┘   └───┘
doc                    └──┘     └───┘
295  lookmap_map_eq _ _ $ by rintro ⟨a₁, b₂⟩ ⟨a₂, b₂⟩;
id   └────────────┘
src  └────────────┘          └──────────────────────┘
typ  └────────────┘          └──────────────────────┘
doc                          └──────────────────────┘
txt                          └──────────────────────┘
par                          └──────────────────────┘
pid                                └────────────────┘
st                          └──────────────────────────
296    dsimp; split_ifs; simp [h] {contextual := tt}
id                                              └┘
src    └───┘  └───────┘  └────┘ └┘ └────────────┘└┘└─
typ    └───┘  └───────┘  └────┘└┘ └────────────┘└┘└─
doc    └───┘  └───────┘  └────┘ └┘ └────────────┘  └─
txt    └───┘  └───────┘  └────┘ └┘ └────────────┘  └─
par    └───┘  └───────┘  └────┘ └┘ └────────────┘  └─
pid                            └────────────┘  
st   ────────────────────────────────────────────────
297  
src  
typ  
doc  
txt  
par  
pid  
st   
298  theorem kreplace_nodupkeys (a : α) (b : β a) {l : list (sigma β)} :
id                                                  └──┘  └───┘ 
src                                                    └──┘  └───┘
typ                                                 └──┘  └───┘ 
299    (kreplace a b l).nodupkeys ↔ l.nodupkeys :=
id      └──────┘    └───────┘   └────────┘
src     └──────┘       └───────┘    └────────┘
typ     └──────┘    └───────┘   └────────┘
300  by simp [nodupkeys, keys_kreplace]
id            └───────┘  └───────────┘
src     └────┘└───────┘└┘└───────────┘└─
typ     └────┘└───────┘└┘└───────────┘└─
doc     └────┘         └┘             └─
txt     └────┘         └┘             └─
par     └────┘         └┘             └─
pid                  └┘             
st     └────────────────────────────────
301  
src  
typ  
doc  
txt  
par  
pid  
st   
302  theorem perm_kreplace {a : α} {b : β a} {l₁ l₂ : list (sigma β)}
id                                                 └──┘  └───┘ 
src                                                   └──┘  └───┘
typ                                                └──┘  └───┘ 
303    (nd : l₁.nodupkeys) : l₁ ~ l₂ →
id           └┘└────────┘    └┘  └┘
src            └────────┘       
typ          └┘└────────┘    └┘  └┘
doc                             
304    kreplace a b l₁ ~ kreplace a b l₂ :=
id     └──────┘   └┘  └──────┘   └┘
src    └──────┘         └──────┘
typ    └──────┘   └┘  └──────┘   └┘
doc                    
305  perm_lookmap _ $ begin
id   └──────────┘
src  └──────────┘
typ  └──────────┘
st                    └─────
306    refine (nodupkeys_iff_pairwise.1 nd).imp _,
id             └────────────────────┘   └┘
src    └─────┘ └────────────────────┘└─┘  └─────┘
typ    └─────┘ └────────────────────┘└─┘└┘└─────┘
doc    └─────┘                       └─┘  └─────┘
txt    └─────┘                       └─┘  └─────┘
par    └─────┘                       └─┘  └─────┘
pid                                 └─┘  └─────┘
st   ───────────────────────────────────────────┘└─
307    intros x y h z h₁ w h₂,
src    └────────────────────┘
typ    └────────────────────┘
doc    └────────────────────┘
txt    └────────────────────┘
par    └────────────────────┘
pid          └──────────────┘
st   ───────────────────────┘└─
308    split_ifs at h₁ h₂; cases h₁; cases h₂,
id                               └┘        └┘
src    └────────────────┘  └────┘    └────┘
typ    └────────────────┘  └────┘└┘  └────┘└┘
doc    └────────────────┘  └────┘    └────┘
txt    └────────────────┘  └────┘    └────┘
par    └────────────────┘  └────┘    └────┘
pid             └───────┘                
st   ───────────────────────────────────────┘└─
309    exact (h (h_2.symm.trans h_1)).elim
id              └────────────┘ └─┘
src    └────┘   └────────────┘   └──────┘
typ    └────┘  └────────────┘└─┘└──────┘
doc    └────┘                    └──────┘
txt    └────┘                    └──────┘
par    └────┘                    └──────┘
pid                             └────┘└┘
st   ─────────────────────────────────────┘
310  end
st   └─┘
311  
312  /- kerase -/
313  
314  /-- Remove the first pair with the key `a`. -/
315  def kerase (a : α) : list (sigma β) → list (sigma β) :=
id                       └──┘  └───┘     └──┘  └───┘ 
src                       └──┘  └───┘      └──┘  └───┘
typ                      └──┘  └───┘     └──┘  └───┘ 
316  erasep $ λ s, a = s.1
id   └────┘         
src  └────┘            
typ  └────┘         
317  
318  @[simp] theorem kerase_nil {a} : @kerase _ β _ a [] = [] :=
id                                     └────┘       └┘  └┘
src                                    └────┘         └┘  └┘
typ                                    └────┘       └┘  └┘
doc    └──┘                            └────┘
319  rfl
id   └─┘
src  └─┘
typ  └─┘
320  
321  @[simp] theorem kerase_cons_eq {a} {s : sigma β} {l : list (sigma β)} (h : a = s.1) :
id                                           └───┘        └──┘  └───┘           
src                                          └───┘         └──┘  └───┘              
typ                                          └───┘        └──┘  └───┘           
doc    └──┘
322    kerase a (s :: l) = l :=
id     └────┘    └┘    
src    └────┘      └┘    
typ    └────┘    └┘    
doc    └────┘
323  by simp [kerase, h]
id            └────┘  
src     └────┘└────┘└┘ └─
typ     └────┘└────┘└┘└─
doc     └────┘└────┘└┘ └─
txt     └────┘      └┘ └─
par     └────┘      └┘ └─
pid               └┘ 
st     └─────────────────
324  
src  
typ  
doc  
txt  
par  
pid  
st   
325  @[simp] theorem kerase_cons_ne {a} {s : sigma β} {l : list (sigma β)} (h : a ≠ s.1) :
id                                           └───┘        └──┘  └───┘           
src                                          └───┘         └──┘  └───┘              
typ                                          └───┘        └──┘  └───┘           
doc    └──┘
326    kerase a (s :: l) = s :: kerase a l :=
id     └────┘    └┘     └┘ └────┘  
src    └────┘      └┘       └┘ └────┘
typ    └────┘    └┘     └┘ └────┘  
doc    └────┘                   └────┘
327  by simp [kerase, h]
id            └────┘  
src     └────┘└────┘└┘ └─
typ     └────┘└────┘└┘└─
doc     └────┘└────┘└┘ └─
txt     └────┘      └┘ └─
par     └────┘      └┘ └─
pid               └┘ 
st     └─────────────────
328  
src  
typ  
doc  
txt  
par  
pid  
st   
329  @[simp] theorem kerase_of_not_mem_keys {a} {l : list (sigma β)} (h : a ∉ l.keys) :
id                                                   └──┘  └───┘           └───┘
src                                                  └──┘  └───┘              └───┘
typ                                                  └──┘  └───┘           └───┘
doc    └──┘                                                                    └───┘
330    kerase a l = l :=
id     └────┘    
src    └────┘     
typ    └────┘    
doc    └────┘
331  by induction l with _ _ ih;
id                
src     └────────┘ └──────────┘
typ     └────────┘└──────────┘
doc     └────────┘ └──────────┘
txt     └────────┘ └──────────┘
par     └────────┘ └──────────┘
pid               └─────────┘
st     └─────────────────────────
332     [refl, { simp [not_or_distrib] at h, simp [h.1, ih h.2] }]
id                    └────────────┘                  └┘ 
src     └──┘    └────┘└────────────┘└────┘  └────┘ └──┘   └──┘
typ     └──┘    └────┘└────────────┘└────┘  └────┘└──┘└┘└──┘
doc      └──┘    └────┘              └────┘  └────┘ └──┘   └──┘
txt      └──┘    └────┘              └────┘  └────┘ └──┘   └──┘
par      └──┘    └────┘              └────┘  └────┘ └──┘   └──┘
pid                                └──┘       └──┘   └─┘
st   ─────────┘└──────────────────────────┘└───────────────────┘└┘
333  
334  theorem kerase_sublist (a : α) (l : list (sigma β)) : kerase a l <+ l :=
id                                      └──┘  └───┘      └────┘   └┘ 
src                                      └──┘  └───┘       └────┘     └┘
typ                                     └──┘  └───┘      └────┘   └┘ 
doc                                                        └────┘
335  erasep_sublist _
id   └────────────┘
src  └────────────┘
typ  └────────────┘
336  
337  theorem kerase_keys_subset (a) (l : list (sigma β)) :
id                                       └──┘  └───┘ 
src                                      └──┘  └───┘
typ                                      └──┘  └───┘ 
338    (kerase a l).keys ⊆ l.keys :=
id      └────┘   └──┘   └───┘
src     └────┘     └──┘    └───┘
typ     └────┘   └──┘   └───┘
doc     └────┘     └──┘     └───┘
339  subset_of_sublist (map_sublist_map _ (kerase_sublist a l))
id   └───────────────┘  └─────────────┘    └────────────┘  
src  └───────────────┘  └─────────────┘    └────────────┘
typ  └───────────────┘  └─────────────┘    └────────────┘  
340  
341  theorem mem_keys_of_mem_keys_kerase {a₁ a₂} {l : list (sigma β)} :
id                                                    └──┘  └───┘ 
src                                                   └──┘  └───┘
typ                                                   └──┘  └───┘ 
342    a₁ ∈ (kerase a₂ l).keys → a₁ ∈ l.keys :=
id     └┘   └────┘ └┘  └──┘    └┘  └───┘
src         └────┘      └──┘         └───┘
typ    └┘   └────┘ └┘  └──┘    └┘  └───┘
doc          └────┘      └──┘          └───┘
343  @kerase_keys_subset _ _ _ _ _ _
id    └────────────────┘
src   └────────────────┘
typ   └────────────────┘
344  
345  theorem exists_of_kerase {a : α} {l : list (sigma β)} (h : a ∈ l.keys) :
id                                        └──┘  └───┘           └───┘
src                                        └──┘  └───┘              └───┘
typ                                       └──┘  └───┘           └───┘
doc                                                                  └───┘
346    ∃ (b : β a) (l₁ l₂ : list (sigma β)),
id                       └──┘  └───┘   
src                        └──┘  └───┘    
typ                      └──┘  └───┘   
347      a ∉ l₁.keys ∧
id         └┘└───┘ 
src           └───┘ 
typ        └┘└───┘ 
doc            └───┘
348      l = l₁ ++ ⟨a, b⟩ :: l₂ ∧
id         └┘ └┘      └┘ └┘ 
src            └┘        └┘    
typ        └┘ └┘      └┘ └┘ 
349      kerase a l = l₁ ++ l₂ :=
id       └────┘    └┘ └┘ └┘
src      └────┘         └┘
typ      └────┘    └┘ └┘ └┘
doc      └────┘
350  begin
st   └─────
351    induction l,
id               
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid             
st   ────────────┘└─
352    case list.nil { cases h },
id                           
src    └──────────────┘└────┘ 
typ    └──────────────┘└────┘
doc    └──────────────┘└────┘ 
txt    └──────────────┘└────┘ 
par    └──────────────┘└────┘ 
pid        └───────┘└──────┘ └┘
st   ────────────────┘└───────┘└┘
353    case list.cons : hd tl ih {
src    └───────────────────────────
typ    └───────────────────────────
doc    └───────────────────────────
txt    └───────────────────────────
par    └───────────────────────────
pid        └────────┘└─────────┘└──
st   ────────────────────────────┘
354      by_cases e : a = hd.1,
id                      └┘
src  ───┘└───────┘ └─┘   └┘└─
typ  ───┘└───────┘ └─┘└┘└┘└─
doc  ───┘└───────┘ └─┘    └┘└─
txt  ───┘└───────┘ └─┘    └┘└─
par  ───┘└───────┘ └─┘    └┘└─
pid  ────────────┘ └─┘    └───
st   ────────────────────────┘└─
355      { subst e,
id               
src  ─────┘└────┘ └─
typ  ─────┘└────┘└─
doc  ─────┘└────┘ └─
txt  ─────┘└────┘ └─
par  ─────┘└────┘ └─
pid  ───────────┘ └─
st   ────┘└──────┘└─
356        exact ⟨hd.2, [], tl, by simp, by cases hd; refl, by simp⟩ },
id                └┘        └┘                    └┘
src  ─────┘└────┘   └──┘  └┘  └┘  └──┘└┘  └────┘  └┘└──┘└┘  └──┘└┘└──
typ  ─────┘└────┘ └┘└──┘  └┘└┘└┘  └──┘└┘  └────┘└┘└┘└──┘└┘  └──┘└┘└──
doc  ─────┘└────┘   └──┘  └┘  └┘  └──┘└┘  └────┘  └┘└──┘└┘  └──┘└┘└──
txt  ─────┘└────┘   └──┘  └┘  └┘  └──┘└┘  └────┘  └┘└──┘└┘  └──┘└┘└──
par  ─────┘└────┘   └──┘  └┘  └┘  └──┘└┘  └────┘  └┘└──┘└┘  └──┘└┘└──
pid  ───────────┘   └──┘  └┘  └┘  └─────┘  └─────┘  └──────┘  └─────────
st   ────────────────────────────┘└───┘└──┘└─────────────┘└──┘└───┘└┘└─
357      { simp at h,
src  ─────┘└───────┘└─
typ  ─────┘└───────┘└─
doc  ─────┘└───────┘└─
txt  ─────┘└───────┘└─
par  ─────┘└───────┘└─
pid  ─────────────────
st   ──────────────┘└─
358        cases h,
id               
src  ─────┘└────┘ └─
typ  ─────┘└────┘└─
doc  ─────┘└────┘ └─
txt  ─────┘└────┘ └─
par  ─────┘└────┘ └─
pid  ───────────┘ └─
st   ────────────┘└─
359        case or.inl : h { exact absurd h e },
id                                 └────┘  
src  ───────────────────────┘└────┘└────┘  └──
typ  ───────────────────────┘└────┘└────┘└──
doc  ───────────────────────┘└────┘        └──
txt  ───────────────────────┘└────┘        └──
par  ───────────────────────┘└────┘        └──
pid  ─────────────────────────────┘        └───
st   ──────────────────────┘└────────────────┘└─
360        case or.inr : h {
src  ────────────────────────
typ  ────────────────────────
doc  ────────────────────────
txt  ────────────────────────
par  ────────────────────────
pid  ────────────────────────
st   ────────────────────────
361          rcases ih h with ⟨b, tl₁, tl₂, h₁, h₂, h₃⟩,
id                  └┘ 
src  ───────┘└─────┘   └─────────────────────────────┘└─
typ  ───────┘└─────┘└┘└─────────────────────────────┘└─
doc  ───────┘└─────┘   └─────────────────────────────┘└─
txt  ───────┘└─────┘   └─────────────────────────────┘└─
par  ───────┘└─────┘   └─────────────────────────────┘└─
pid  ──────────────┘   └────────────────────────────────
st   ─────────────────────────────────────────────────┘└─
362          exact ⟨b, hd :: tl₁, tl₂, not_mem_cons_of_ne_of_not_mem e h₁,
id                    └┘    └─┘  └─┘  └───────────────────────────┘  └┘
src  ───────┘└────┘  └┘       └┘   └┘└───────────────────────────┘   └─
typ  ───────┘└────┘ └┘└┘  └─┘└┘└─┘└┘└───────────────────────────┘└┘└─
doc  ───────┘└────┘  └┘       └┘   └┘                                └─
txt  ───────┘└────┘  └┘       └┘   └┘                                └─
par  ───────┘└────┘  └┘       └┘   └┘                                └─
pid  ─────────────┘  └┘       └┘   └┘                                └─
st   ──────────────────────────────────────────────────────────────────────
363                 by rw h₂; refl, by simp [e, h₃]⟩ } } }
id                        └┘                   └┘
src  ──────────────┘  └─┘  └┘└──┘└┘  └────┘ └┘  └┘└────┘
typ  ──────────────┘  └─┘└┘└┘└──┘└┘  └────┘└┘└┘└┘└────┘
doc  ──────────────┘  └─┘  └┘└──┘└┘  └────┘ └┘  └┘└────┘
txt  ──────────────┘  └─┘  └┘└──┘└┘  └────┘ └┘  └┘└────┘
par  ──────────────┘  └─┘  └┘└──┘└┘  └────┘ └┘  └┘└────┘
pid  ──────────────┘  └──┘  └──────┘  └─────┘ └┘  └──────┘
st   ────────────────┘└──────────┘└──┘└───────────┘└┘└─┘
364  end
st   └─┘
365  
366  @[simp] theorem mem_keys_kerase_of_ne {a₁ a₂} {l : list (sigma β)} (h : a₁ ≠ a₂) :
id                                                      └──┘  └───┘         └┘  └┘
src                                                     └──┘  └───┘             
typ                                                     └──┘  └───┘         └┘  └┘
doc    └──┘
367    a₁ ∈ (kerase a₂ l).keys ↔ a₁ ∈ l.keys :=
id     └┘   └────┘ └┘  └──┘   └┘  └───┘
src         └────┘      └──┘        └───┘
typ    └┘   └────┘ └┘  └──┘   └┘  └───┘
doc          └────┘      └──┘          └───┘
368  iff.intro mem_keys_of_mem_keys_kerase $ λ p,
id   └───────┘ └─────────────────────────┘     
src  └───────┘ └─────────────────────────┘
typ  └───────┘ └─────────────────────────┘     
369    if q : a₂ ∈ l.keys then
id     └┘     └┘  └───┘
src    └┘          └───┘
typ    └┘     └┘  └───┘
doc                 └───┘
370      match l, kerase a₂ l, exists_of_kerase q, p with
id               └────┘ └┘   └──────────────┘   
src               └────┘       └──────────────┘
typ              └────┘ └┘   └──────────────┘   
doc               └────┘
371      | _, _, ⟨_, _, _, _, rfl, rfl⟩, p := by simpa [keys, h] using p
id                                 └─┘                  └──┘          
src                                └─┘           └─────┘└──┘└┘ └──────┘ 
typ                                └─┘           └─────┘└──┘└┘└──────┘
doc                                              └─────┘└──┘└┘ └──────┘ 
txt                                              └─────┘    └┘ └──────┘ 
par                                              └─────┘    └┘ └──────┘ 
pid                                                       └┘ └────┘ 
st                                              └────────────────────────
372      end
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘
373    else
374      by simp [q, p]
id                  
src         └────┘ └┘ └─
typ         └────┘└┘└─
doc         └────┘ └┘ └─
txt         └────┘ └┘ └─
par         └────┘ └┘ └─
pid              └┘ 
st         └────────────
375  
src  
typ  
doc  
txt  
par  
pid  
st   
376  theorem keys_kerase {a} {l : list (sigma β)} : (kerase a l).keys = l.keys.erase a :=
id                                └──┘  └───┘       └────┘   └──┘   └───┘└────┘ 
src                               └──┘  └───┘        └────┘     └──┘    └───┘└────┘
typ                               └──┘  └───┘       └────┘   └──┘   └───┘└────┘ 
doc                                                  └────┘     └──┘     └───┘
377  by rw [keys, kerase, ←erasep_map sigma.fst l, erase_eq_erasep]
id          └──┘  └────┘   └────────┘ └───────┘   └─────────────┘
src     └──┘└──┘└┘└────┘└─┘└────────┘└───────┘ └┘└─────────────┘└─
typ     └──┘└──┘└┘└────┘└─┘└────────┘└───────┘└┘└─────────────┘└─
doc     └──┘└──┘└┘└────┘└─┘                    └┘               └─
txt     └──┘    └┘      └─┘                    └┘               └─
par     └──┘    └┘      └─┘                    └┘               └─
pid       └┘    └┘      └─┘                    └┘               
st     └───────┘└──────┘└───────────────────────┘└───────────────┘
378  
src  
typ  
doc  
txt  
par  
pid  
st   
379  theorem kerase_kerase {a a'} {l : list (sigma β)} : (kerase a' l).kerase a = (kerase a l).kerase a' :=
id                                     └──┘  └───┘       └────┘ └┘  └────┘     └────┘   └────┘  └┘
src                                    └──┘  └───┘        └────┘      └────┘      └────┘     └────┘
typ                                    └──┘  └───┘       └────┘ └┘  └────┘     └────┘   └────┘  └┘
doc                                                       └────┘      └────┘       └────┘     └────┘
380  begin
st   └─────
381    by_cases a = a',
id                └┘
src    └───────┘ 
typ    └───────┘└┘
doc    └───────┘  
txt    └───────┘  
par    └───────┘  
pid              
st   ────────────────┘└─
382    { subst a' },
id             └┘
src      └────┘  
typ      └────┘└┘
doc      └────┘  
txt      └────┘  
par      └────┘  
pid             
st   ───┘└───────┘└┘
383    induction l with x xs, { refl },
id               
src    └────────┘ └────────┘    └───┘
typ    └────────┘└────────┘    └───┘
doc    └────────┘ └────────┘    └───┘
txt    └────────┘ └────────┘    └───┘
par    └────────┘ └────────┘    └───┘
pid              └───────┘        
st   ──────────────────────┘└──┘└───┘└┘
384    { by_cases a' = x.1,
id                └┘   
src      └───────┘    └┘
typ      └───────┘└┘ └┘
doc      └───────┘    └┘
txt      └───────┘    └┘
par      └───────┘    └┘
pid                  └┘
st   ────────────────────┘└─
385      { subst a', simp [kerase_cons_ne h,kerase_cons_eq rfl] },
id               └┘        └────────────┘  └────────────┘ └─┘
src        └────┘    └────┘└────────────┘ └────────────┘└─┘└┘
typ        └────┘└┘  └────┘└────────────┘└────────────┘└─┘└┘
doc        └────┘    └────┘                                └┘
txt        └────┘    └────┘                                └┘
par        └────┘    └────┘                                └┘
pid                                                     
st   ─────┘└──────┘└───────────────────────────────────────────┘└┘
386      by_cases h' : a = x.1,
id                        
src      └───────┘  └─┘   └┘
typ      └───────┘  └─┘ └┘
doc      └───────┘  └─┘   └┘
txt      └───────┘  └─┘   └┘
par      └───────┘  └─┘   └┘
pid                └─┘   └┘
st   ────────────────────────┘└─
387      { subst a, simp [kerase_cons_eq rfl,kerase_cons_ne (ne.symm h)] },
id                       └────────────┘ └─┘ └────────────┘  └─────┘ 
src        └────┘   └────┘└────────────┘└─┘└────────────┘ └─────┘ └─┘
typ        └────┘  └────┘└────────────┘└─┘└────────────┘ └─────┘└─┘
doc        └────┘   └────┘                                        └─┘
txt        └────┘   └────┘                                        └─┘
par        └────┘   └────┘                                        └─┘
pid                                                            └┘
st   ─────┘└─────┘└─────────────────────────────────────────────────────┘└┘
388      { simp [kerase_cons_ne,*] } }
id               └────────────┘
src        └────┘└────────────┘└──┘
typ        └────┘└────────────┘└──┘
doc        └────┘              └──┘
txt        └────┘              └──┘
par        └────┘              └──┘
pid                          └─┘
st   ─────────────────────────────┘└───
389  end
st   ──┘
390  
391  theorem kerase_nodupkeys (a : α) {l : list (sigma β)} : nodupkeys l → (kerase a l).nodupkeys :=
id                                        └──┘  └───┘      └───────┘     └────┘   └───────┘
src                                        └──┘  └───┘       └───────┘      └────┘     └───────┘
typ                                       └──┘  └───┘      └───────┘     └────┘   └───────┘
doc                                                                         └────┘
392  nodupkeys_of_sublist $ kerase_sublist _ _
id   └──────────────────┘   └────────────┘
src  └──────────────────┘   └────────────┘
typ  └──────────────────┘   └────────────┘
393  
394  theorem perm_kerase {a : α} {l₁ l₂ : list (sigma β)}
id                                       └──┘  └───┘ 
src                                       └──┘  └───┘
typ                                      └──┘  └───┘ 
395    (nd : l₁.nodupkeys) : l₁ ~ l₂ → kerase a l₁ ~ kerase a l₂ :=
id           └┘└────────┘    └┘  └┘   └────┘  └┘  └────┘  └┘
src            └────────┘             └────┘       └────┘
typ          └┘└────────┘    └┘  └┘   └────┘  └┘  └────┘  └┘
doc                                   └────┘       └────┘
396  perm_erasep _ $ (nodupkeys_iff_pairwise.1 nd).imp $
id   └─────────┘      └────────────────────┘  └┘ └─┘
src  └─────────┘      └────────────────────┘     └─┘
typ  └─────────┘      └────────────────────┘  └┘ └─┘
397  by rintro x y h rfl; exact h
id                              
src     └──────────────┘  └────┘ 
typ     └──────────────┘  └────┘
doc     └──────────────┘  └────┘ 
txt     └──────────────┘  └────┘ 
par     └──────────────┘  └────┘ 
pid           └────────┘        
st     └──────────────────────────
398  
src  
typ  
doc  
txt  
par  
pid  
st   
399  @[simp] theorem not_mem_keys_kerase (a) {l : list (sigma β)} (nd : l.nodupkeys) :
id                                                └──┘  └───┘          └────────┘
src                                               └──┘  └───┘            └────────┘
typ                                               └──┘  └───┘          └────────┘
doc    └──┘
400    a ∉ (kerase a l).keys :=
id        └────┘   └──┘
src        └────┘     └──┘
typ       └────┘   └──┘
doc         └────┘     └──┘
401  begin
st   └─────
402    induction l,
id               
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid             
st   ────────────┘└─
403    case list.nil { simp },
src    └──────────────┘└───┘
typ    └──────────────┘└───┘
doc    └──────────────┘└───┘
txt    └──────────────┘└───┘
par    └──────────────┘└───┘
pid        └───────┘└──────┘
st   ────────────────┘└────┘└┘
404    case list.cons : hd tl ih {
src    └───────────────────────────
typ    └───────────────────────────
doc    └───────────────────────────
txt    └───────────────────────────
par    └───────────────────────────
pid        └────────┘└─────────┘└──
st   ────────────────────────────┘
405      simp at nd,
src  ───┘└────────┘└─
typ  ───┘└────────┘└─
doc  ───┘└────────┘└─
txt  ───┘└────────┘└─
par  ───┘└────────┘└─
pid  ────────────────
st   ─────────────┘└─
406      by_cases h : a = hd.1,
id                      └┘
src  ───┘└───────┘ └─┘   └┘└─
typ  ───┘└───────┘ └─┘└┘└┘└─
doc  ───┘└───────┘ └─┘    └┘└─
txt  ───┘└───────┘ └─┘    └┘└─
par  ───┘└───────┘ └─┘    └┘└─
pid  ────────────┘ └─┘    └───
st   ────────────────────────┘└─
407      { subst h, simp [nd.1] },
id                       └┘
src  ─────┘└────┘ └┘└────┘  └──┘└──
typ  ─────┘└────┘└┘└────┘└┘└──┘└──
doc  ─────┘└────┘ └┘└────┘  └──┘└──
txt  ─────┘└────┘ └┘└────┘  └──┘└──
par  ─────┘└────┘ └┘└────┘  └──┘└──
pid  ───────────┘ └──────┘  └──────
st   ────┘└──────┘└────────────┘└─
408      { simp [h, ih nd.2] } }
id                 └┘ └┘
src  ─────┘└────┘ └┘    └──┘└──┘
typ  ─────┘└────┘└┘└┘└┘└──┘└──┘
doc  ─────┘└────┘ └┘    └──┘└──┘
txt  ─────┘└────┘ └┘    └──┘└──┘
par  ─────┘└────┘ └┘    └──┘└──┘
pid  ───────────┘ └┘    └─────┘
st   ───────────────────────┘└─┘
409  end
st   └─┘
410  
411  @[simp] theorem lookup_kerase (a) {l : list (sigma β)} (nd : l.nodupkeys) :
id                                          └──┘  └───┘          └────────┘
src                                         └──┘  └───┘            └────────┘
typ                                         └──┘  └───┘          └────────┘
doc    └──┘
412    lookup a (kerase a l) = none :=
id     └────┘   └────┘     └──┘
src    └────┘    └────┘       └──┘
typ    └────┘   └────┘     └──┘
doc    └────┘    └────┘
413  lookup_eq_none.mpr (not_mem_keys_kerase a nd)
id   └────────────┘└──┘  └─────────────────┘  └┘
src  └────────────┘└──┘  └─────────────────┘
typ  └────────────┘└──┘  └─────────────────┘  └┘
414  
415  @[simp] theorem lookup_kerase_ne {a a'} {l : list (sigma β)} (h : a ≠ a') :
id                                                └──┘  └───┘           └┘
src                                               └──┘  └───┘            
typ                                               └──┘  └───┘           └┘
doc    └──┘
416    lookup a (kerase a' l) = lookup a l :=
id     └────┘   └────┘ └┘    └────┘  
src    └────┘    └────┘        └────┘
typ    └────┘   └────┘ └┘    └────┘  
doc    └────┘    └────┘         └────┘
417  begin
st   └─────
418    induction l,
id               
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid             
st   ────────────┘└─
419    case list.nil { refl },
src    └──────────────┘└───┘
typ    └──────────────┘└───┘
doc    └──────────────┘└───┘
txt    └──────────────┘└───┘
par    └──────────────┘└───┘
pid        └───────┘└──────┘
st   ────────────────┘└────┘└┘
420    case list.cons : hd tl ih {
src    └───────────────────────────
typ    └───────────────────────────
doc    └───────────────────────────
txt    └───────────────────────────
par    └───────────────────────────
pid        └────────┘└─────────┘└──
st   ────────────────────────────┘
421      cases hd with ah bh,
id             └┘
src  ───┘└────┘  └─────────┘└─
typ  ───┘└────┘└┘└─────────┘└─
doc  ───┘└────┘  └─────────┘└─
txt  ───┘└────┘  └─────────┘└─
par  ───┘└────┘  └─────────┘└─
pid  ─────────┘  └────────────
st   ──────────────────────┘└─
422      by_cases h₁ : a = ah; by_cases h₂ : a' = ah,
id                       └┘                └┘   └┘
src  ───┘└───────┘  └─┘   └┘└───────┘  └─┘     └─
typ  ───┘└───────┘  └─┘└┘└┘└───────┘  └─┘└┘ └┘└─
doc  ───┘└───────┘  └─┘    └┘└───────┘  └─┘     └─
txt  ───┘└───────┘  └─┘    └┘└───────┘  └─┘     └─
par  ───┘└───────┘  └─┘    └┘└───────┘  └─┘     └─
pid  ────────────┘  └─┘    └─────────┘  └─┘     └─
st   ──────────────────────────────────────────────┘└─
423      { substs h₁ h₂, cases ne.irrefl h },
id                             └───────┘ 
src  ─────┘└──────────┘└┘└────┘└───────┘ └──
typ  ─────┘└──────────┘└┘└────┘└───────┘└──
doc  ─────┘└──────────┘└┘└────┘          └──
txt  ─────┘└──────────┘└┘└────┘          └──
par  ─────┘└──────────┘└┘└────┘          └──
pid  ─────────────────────────┘          └───
st   ────┘└───────────┘└──────────────────┘└─
424      { subst h₁, simp [h₂] },
id               └┘        └┘
src  ─────┘└────┘  └┘└────┘  └┘└──
typ  ─────┘└────┘└┘└┘└────┘└┘└┘└──
doc  ─────┘└────┘  └┘└────┘  └┘└──
txt  ─────┘└────┘  └┘└────┘  └┘└──
par  ─────┘└────┘  └┘└────┘  └┘└──
pid  ───────────┘  └──────┘  └────
st   ────┘└───────┘└──────────┘└─
425      { subst h₂, simp [h] },
id               └┘        
src  ─────┘└────┘  └┘└────┘ └┘└──
typ  ─────┘└────┘└┘└┘└────┘└┘└──
doc  ─────┘└────┘  └┘└────┘ └┘└──
txt  ─────┘└────┘  └┘└────┘ └┘└──
par  ─────┘└────┘  └┘└────┘ └┘└──
pid  ───────────┘  └──────┘ └────
st   ────┘└───────┘└─────────┘└─
426      { simp [h₁, h₂, ih] }
id               └┘  └┘  └┘
src  ─────┘└────┘  └┘  └┘  └┘└─
typ  ─────┘└────┘└┘└┘└┘└┘└┘└┘└─
doc  ─────┘└────┘  └┘  └┘  └┘└─
txt  ─────┘└────┘  └┘  └┘  └┘└─
par  ─────┘└────┘  └┘  └┘  └┘└─
pid  ───────────┘  └┘  └┘  └───
st   ───────────────────────┘└─
427    }
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ──┘
st   ──┘
428  end
st   └─┘
429  
430  theorem kerase_append_left {a} : ∀ {l₁ l₂ : list (sigma β)},
id                                              └──┘  └───┘ 
src                                              └──┘  └───┘
typ                                             └──┘  └───┘ 
431    a ∈ l₁.keys → kerase a (l₁ ++ l₂) = kerase a l₁ ++ l₂
id       └┘└───┘   └────┘   └┘ └┘ └┘   └────┘  └┘ └┘ └┘
src         └───┘   └────┘       └┘      └────┘      └┘
typ      └┘└───┘   └────┘   └┘ └┘ └┘   └────┘  └┘ └┘ └┘
doc          └───┘   └────┘                └────┘
432  | []        _  h  := by cases h
id     └┘                          
src    └┘                    └────┘ 
typ    └┘                    └────┘
doc                          └────┘ 
txt                          └────┘ 
par                          └────┘ 
pid                                
st                          └───────┘
433  | (s :: l₁) l₂ h₁ :=
id       └┘
src       └┘
typ      └┘
434    if h₂ : a = s.1 then
id     └┘         
src    └┘          
typ    └┘         
435      by simp [h₂]
id                └┘
src         └────┘  └─
typ         └────┘└┘└─
doc         └────┘  └─
txt         └────┘  └─
par         └────┘  └─
pid               
st         └──────────
436    else
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
437      by simp at h₁;
src         └────────┘
typ         └────────┘
doc         └────────┘
txt         └────────┘
par         └────────┘
pid             └───┘
st         └────────────
438         cases h₁;
id                └┘
src         └────┘
typ         └────┘└┘
doc         └────┘
txt         └────┘
par         └────┘
pid              
st   ─────────────────
439         [exact absurd h₁ h₂, simp [h₂, kerase_append_left h₁]]
id                └────┘ └┘ └┘        └┘  └────────────────┘ └┘
src         └────┘└────┘      └────┘  └┘                    
typ         └────┘└────┘└┘└┘  └────┘└┘└┘└────────────────┘└┘
doc          └────┘            └────┘  └┘                    
txt          └────┘            └────┘  └┘                    
par          └────┘            └────┘  └┘                    
pid                                 └┘                    
st   ────────────────────────────────────────────────────────────┘
440  
441  theorem kerase_append_right {a} : ∀ {l₁ l₂ : list (sigma β)},
id                                               └──┘  └───┘ 
src                                               └──┘  └───┘
typ                                              └──┘  └───┘ 
442    a ∉ l₁.keys → kerase a (l₁ ++ l₂) = l₁ ++ kerase a l₂
id       └┘└───┘   └────┘   └┘ └┘ └┘   └┘ └┘ └────┘  └┘
src         └───┘   └────┘       └┘         └┘ └────┘
typ      └┘└───┘   └────┘   └┘ └┘ └┘   └┘ └┘ └────┘  └┘
doc          └───┘   └────┘                      └────┘
443  | []        _  h := rfl
id     └┘                └─┘
src    └┘                └─┘
typ    └┘                └─┘
444  | (_ :: l₁) l₂ h := by simp [not_or_distrib] at h;
id        └┘                      └────────────┘
src       └┘                └────┘└────────────┘└────┘
typ       └┘                └────┘└────────────┘└────┘
doc                         └────┘              └────┘
txt                         └────┘              └────┘
par                         └────┘              └────┘
pid                                           └──┘
st                         └────────────────────────────
445                         simp [h.1, kerase_append_right h.2]
id                                    └─────────────────┘ 
src                         └────┘ └──┘                    └───
typ                         └────┘└──┘└─────────────────┘└───
doc                         └────┘ └──┘                    └───
txt                         └────┘ └──┘                    └───
par                         └────┘ └──┘                    └───
pid                              └──┘                    └─┘
st   ───────────────────────────────────────────────────────────
446  
src  
typ  
doc  
txt  
par  
pid  
st   
447  theorem kerase_comm (a₁ a₂) (l : list (sigma β)) :
id                                    └──┘  └───┘ 
src                                   └──┘  └───┘
typ                                   └──┘  └───┘ 
448    kerase a₂ (kerase a₁ l) = kerase a₁ (kerase a₂ l) :=
id     └────┘ └┘  └────┘ └┘    └────┘ └┘  └────┘ └┘ 
src    └────┘     └────┘        └────┘     └────┘
typ    └────┘ └┘  └────┘ └┘    └────┘ └┘  └────┘ └┘ 
doc    └────┘     └────┘         └────┘     └────┘
449  if h : a₁ = a₂ then
id   └┘     └┘  └┘
src  └┘        
typ  └┘     └┘  └┘
450    by simp [h]
id              
src       └────┘ └┘
typ       └────┘└┘
doc       └────┘ └┘
txt       └────┘ └┘
par       └────┘ └┘
pid            
st       └────────┘
451  else if ha₁ : a₁ ∈ l.keys then
id        └┘       └┘  └───┘
src       └┘            └───┘
typ       └┘       └┘  └───┘
doc                      └───┘
452    if ha₂ : a₂ ∈ l.keys then
id     └┘       └┘  └───┘
src    └┘            └───┘
typ    └┘       └┘  └───┘
doc                   └───┘
453      match l, kerase a₁ l, exists_of_kerase ha₁, ha₂ with
id               └────┘ └┘   └──────────────┘ └─┘  └─┘
src               └────┘       └──────────────┘
typ              └────┘ └┘   └──────────────┘ └─┘  └─┘
doc               └────┘
454      | _, _, ⟨b₁, l₁, l₂, a₁_nin_l₁, rfl, rfl⟩, a₂_in_l₁_app_l₂ :=
id                    └┘                      └─┘
src                                           └─┘
typ                   └┘                      └─┘
455        if h' : a₂ ∈ l₁.keys then
id         └┘      └┘    └───┘
src        └┘            └───┘
typ        └┘      └┘    └───┘
doc                       └───┘
456          by simp [kerase_append_left h',
id                    └────────────────┘ └┘
src             └────┘└────────────────┘  └─
typ             └────┘└────────────────┘└┘└─
doc             └────┘                    └─
txt             └────┘                    └─
par             └────┘                    └─
pid                                     └─
st             └─────────────────────────────
457                   kerase_append_right (mt (mem_keys_kerase_of_ne h).mp a₁_nin_l₁)]
id                    └─────────────────┘  └┘  └───────────────────┘      └───────┘
src  ────────────────┘└─────────────────┘ └┘ └───────────────────┘ └───┘         └──
typ  ────────────────┘└─────────────────┘ └┘ └───────────────────┘└───┘└───────┘└──
doc  ────────────────┘                                             └───┘         └──
txt  ────────────────┘                                             └───┘         └──
par  ────────────────┘                                             └───┘         └──
pid  ────────────────┘                                             └───┘         └┘
st   ──────────────────────────────────────────────────────────────────────────────────
458        else
src  ─────┘
typ  ─────┘
doc  ─────┘
txt  ─────┘
par  ─────┘
pid  ─────┘
st   ─────┘
459          by simp [kerase_append_right h', kerase_append_right a₁_nin_l₁,
id                    └─────────────────┘ └┘  └─────────────────┘ └───────┘
src             └────┘└─────────────────┘  └┘└─────────────────┘         └─
typ             └────┘└─────────────────┘└┘└┘└─────────────────┘└───────┘└─
doc             └────┘                     └┘                            └─
txt             └────┘                     └┘                            └─
par             └────┘                     └┘                            └─
pid                                      └┘                            └─
st             └─────────────────────────────────────────────────────────────
460                   @kerase_cons_ne _ _ _ a₂ ⟨a₁, b₁⟩ _ (ne.symm h)]
id                     └────────────┘       └┘  └┘  └┘     └─────┘ 
src  ────────────────┘ └────────────┘└─────┘     └┘  └──┘ └─────┘ └──
typ  ────────────────┘ └────────────┘└─────┘└┘ └┘└┘└┘└──┘ └─────┘└──
doc  ────────────────┘               └─────┘     └┘  └──┘         └──
txt  ────────────────┘               └─────┘     └┘  └──┘         └──
par  ────────────────┘               └─────┘     └┘  └──┘         └──
pid  ────────────────┘               └─────┘     └┘  └──┘         └┘
st   ──────────────────────────────────────────────────────────────────
461      end
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘
462    else
463      by simp [ha₂, mt mem_keys_of_mem_keys_kerase ha₂]
id                └─┘  └┘ └─────────────────────────┘ └─┘
src         └────┘   └┘└┘└─────────────────────────┘   └┘
typ         └────┘└─┘└┘└┘└─────────────────────────┘└─┘└┘
doc         └────┘   └┘                                └┘
txt         └────┘   └┘                                └┘
par         └────┘   └┘                                └┘
pid                └┘                                
st         └──────────────────────────────────────────────┘
464  else
465    by simp [ha₁, mt mem_keys_of_mem_keys_kerase ha₁]
id              └─┘  └┘ └─────────────────────────┘ └─┘
src       └────┘   └┘└┘└─────────────────────────┘   └─
typ       └────┘└─┘└┘└┘└─────────────────────────┘└─┘└─
doc       └────┘   └┘                                └─
txt       └────┘   └┘                                └─
par       └────┘   └┘                                └─
pid              └┘                                
st       └───────────────────────────────────────────────
466  
src  
typ  
doc  
txt  
par  
pid  
st   
467  /- kinsert -/
src  ──────────────
typ  ──────────────
doc  ──────────────
txt  ──────────────
par  ──────────────
pid  ──────────────
st   ──────────────
468  
src  
typ  
doc  
txt  
par  
pid  
st   
469  /-- Insert the pair `⟨a, b⟩` and erase the first pair with the key `a`. -/
470  def kinsert (a : α) (b : β a) (l : list (sigma β)) : list (sigma β) :=
id                                   └──┘  └───┘      └──┘  └───┘ 
src                                     └──┘  └───┘       └──┘  └───┘
typ                                  └──┘  └───┘      └──┘  └───┘ 
471  ⟨a, b⟩ :: kerase a l
id        └┘ └────┘  
src         └┘ └────┘
typ       └┘ └────┘  
doc            └────┘
472  
473  @[simp] theorem kinsert_def {a} {b : β a} {l : list (sigma β)} :
id                                                └──┘  └───┘ 
src                                                 └──┘  └───┘
typ                                               └──┘  └───┘ 
doc    └──┘
474    kinsert a b l = ⟨a, b⟩ :: kerase a l := rfl
id     └─────┘          └┘ └────┘      └─┘
src    └─────┘               └┘ └────┘        └─┘
typ    └─────┘          └┘ └────┘      └─┘
doc    └─────┘                   └────┘
475  
476  @[simp] theorem mem_keys_kinsert {a a'} {b' : β a'} {l : list (sigma β)} :
id                                                  └┘       └──┘  └───┘ 
src                                                           └──┘  └───┘
typ                                                 └┘       └──┘  └───┘ 
doc    └──┘
477    a ∈ (kinsert a' b' l).keys ↔ a = a' ∨ a ∈ l.keys :=
id        └─────┘ └┘ └┘  └──┘     └┘    └───┘
src        └─────┘         └──┘              └───┘
typ       └─────┘ └┘ └┘  └──┘     └┘    └───┘
doc         └─────┘         └──┘                  └───┘
478  by by_cases h : a = a'; simp [h]
id                     └┘        
src     └───────┘ └─┘     └────┘ └─
typ     └───────┘ └─┘└┘  └────┘└─
doc     └───────┘ └─┘      └────┘ └─
txt     └───────┘ └─┘      └────┘ └─
par     └───────┘ └─┘      └────┘ └─
pid              └─┘           
st     └──────────────────────────────
479  
src  
typ  
doc  
txt  
par  
pid  
st   
480  theorem kinsert_nodupkeys (a) (b : β a) {l : list (sigma β)} (nd : l.nodupkeys) :
id                                              └──┘  └───┘          └────────┘
src                                               └──┘  └───┘            └────────┘
typ                                             └──┘  └───┘          └────────┘
481    (kinsert a b l).nodupkeys :=
id      └─────┘    └───────┘
src     └─────┘       └───────┘
typ     └─────┘    └───────┘
doc     └─────┘
482  nodupkeys_cons.mpr ⟨not_mem_keys_kerase a nd, kerase_nodupkeys a nd⟩
id   └────────────┘└──┘  └─────────────────┘  └┘  └──────────────┘  └┘
src  └────────────┘└──┘  └─────────────────┘       └──────────────┘
typ  └────────────┘└──┘  └─────────────────┘  └┘  └──────────────┘  └┘
483  
484  theorem perm_kinsert {a} {b : β a} {l₁ l₂ : list (sigma β)} (nd₁ : l₁.nodupkeys)
id                                             └──┘  └───┘           └┘└────────┘
src                                              └──┘  └───┘              └────────┘
typ                                            └──┘  └───┘           └┘└────────┘
485    (p : l₁ ~ l₂) : kinsert a b l₁ ~ kinsert a b l₂ :=
id          └┘  └┘    └─────┘   └┘  └─────┘   └┘
src                   └─────┘         └─────┘
typ         └┘  └┘    └─────┘   └┘  └─────┘   └┘
doc                   └─────┘         └─────┘
486  perm.skip ⟨a, b⟩ $ perm_kerase nd₁ p
id   └───────┘        └─────────┘ └─┘ 
src  └───────┘          └─────────┘
typ  └───────┘        └─────────┘ └─┘ 
487  
488  @[simp] theorem lookup_kinsert {a} {b : β a} (l : list (sigma β)) :
id                                                   └──┘  └───┘ 
src                                                    └──┘  └───┘
typ                                                  └──┘  └───┘ 
doc    └──┘
489    lookup a (kinsert a b l) = some b :=
id     └────┘   └─────┘      └──┘ 
src    └────┘    └─────┘         └──┘
typ    └────┘   └─────┘      └──┘ 
doc    └────┘    └─────┘
490  by simp only [kinsert, lookup_cons_eq]
id                 └─────┘  └────────────┘
src     └─────────┘└─────┘└┘└────────────┘└─
typ     └─────────┘└─────┘└┘└────────────┘└─
doc     └─────────┘└─────┘└┘              └─
txt     └─────────┘       └┘              └─
par     └─────────┘       └┘              └─
pid         └──┘└┘       └┘              
st     └────────────────────────────────────
491  
src  
typ  
doc  
txt  
par  
pid  
st   
492  @[simp] theorem lookup_kinsert_ne {a a'} {b' : β a'} {l : list (sigma β)} (h : a ≠ a') :
id                                                   └┘       └──┘  └───┘           └┘
src                                                            └──┘  └───┘            
typ                                                  └┘       └──┘  └───┘           └┘
doc    └──┘
493    lookup a (kinsert a' b' l) = lookup a l :=
id     └────┘   └─────┘ └┘ └┘    └────┘  
src    └────┘    └─────┘           └────┘
typ    └────┘   └─────┘ └┘ └┘    └────┘  
doc    └────┘    └─────┘            └────┘
494  by simp [h, lookup_cons_ne _ ⟨a', b'⟩ h]
id              └────────────┘    └┘  └┘  
src     └────┘ └┘└────────────┘└─┘   └┘  └┘ └─
typ     └────┘└┘└────────────┘└─┘ └┘└┘└┘└┘└─
doc     └────┘ └┘              └─┘   └┘  └┘ └─
txt     └────┘ └┘              └─┘   └┘  └┘ └─
par     └────┘ └┘              └─┘   └┘  └┘ └─
pid          └┘              └─┘   └┘  └┘ 
st     └──────────────────────────────────────
495  
src  
typ  
doc  
txt  
par  
pid  
st   
496  /- kextract -/
src  ───────────────
typ  ───────────────
doc  ───────────────
txt  ───────────────
par  ───────────────
pid  ───────────────
st   ───────────────
497  
src  
typ  
doc  
txt  
par  
pid  
st   
498  def kextract (a : α) : list (sigma β) → option (β a) × list (sigma β)
id                         └──┘  └───┘    └────┘      └──┘  └───┘ 
src                         └──┘  └───┘      └────┘        └──┘  └───┘
typ                        └──┘  └───┘    └────┘      └──┘  └───┘ 
499  | []     := (none, [])
id     └┘        └──┘  └┘
src    └┘        └──┘  └┘
typ    └┘        └──┘  └┘
500  | (s::l) := if h : s.1 = a then (some (eq.rec_on h s.2), l) else
id      └┘     └┘               └──┘  └───────┘   
src      └┘      └┘                └──┘  └───────┘    
typ     └┘     └┘               └──┘  └───────┘   
501    let (b', l') := kextract l in (b', s :: l')
id     └─┘ └┘  └┘     └──────┘            └┘
src                                       └┘
typ    └─┘ └┘  └┘     └──────┘            └┘
502  
503  @[simp] theorem kextract_eq_lookup_kerase (a : α) :
id                                                  
typ                                                 
doc    └──┘
504    ∀ l : list (sigma β), kextract a l = (lookup a l, kerase a l)
id          └──┘  └───┘    └──────┘    └────┘    └────┘  
src          └──┘  └───┘     └──────┘      └────┘      └────┘
typ         └──┘  └───┘    └──────┘    └────┘    └────┘  
doc                                          └────┘      └────┘
505  | []     := rfl
id     └┘        └─┘
src    └┘        └─┘
typ    └┘        └─┘
506  | (⟨a', b⟩::l) := begin
id             └┘
src            └┘
typ            └┘
st                     └─────
507      simp [kextract], dsimp, split_ifs,
id             └──────┘
src      └────┘└──────┘  └───┘  └───────┘
typ      └────┘└──────┘  └───┘  └───────┘
doc      └────┘          └───┘  └───────┘
txt      └────┘          └───┘  └───────┘
par      └────┘          └───┘  └───────┘
pid                  
st   ──────────────────┘└─────┘└─────────┘└─
508      { subst a', simp [kerase] },
id               └┘        └────┘
src        └────┘    └────┘└────┘└┘
typ        └────┘└┘  └────┘└────┘└┘
doc        └────┘    └────┘└────┘└┘
txt        └────┘    └────┘      └┘
par        └────┘    └────┘      └┘
pid                           
st   ─────┘└──────┘└──────────────┘└┘
509      { simp [kextract, ne.symm h, kextract_eq_lookup_kerase l, kerase] }
id               └──────┘  └─────┘   └───────────────────────┘   └────┘
src        └────┘└──────┘└┘└─────┘ └┘                          └┘└────┘└┘
typ        └────┘└──────┘└┘└─────┘└┘└───────────────────────┘└┘└────┘└┘
doc        └────┘        └┘        └┘                          └┘└────┘└┘
txt        └────┘        └┘        └┘                          └┘      └┘
par        └────┘        └┘        └┘                          └┘      └┘
pid                    └┘        └┘                          └┘      
st   ─────────────────────────────────────────────────────────────────────┘└─
510    end
st   ────┘
511  
512  /- erase_dupkeys -/
513  
514  def erase_dupkeys : list (sigma β) → list (sigma β) :=
id                       └──┘  └───┘     └──┘  └───┘ 
src                      └──┘  └───┘      └──┘  └───┘
typ                      └──┘  └───┘     └──┘  └───┘ 
515  list.foldr (λ ⟨x,y⟩, kinsert x y) []
id   └────────┘        └─────┘      └┘
src  └────────┘           └─────┘      └┘
typ  └────────┘        └─────┘      └┘
doc                       └─────┘
516  
517  lemma erase_dupkeys_cons {x : α} {y : β x} (l : list (sigma β)) : erase_dupkeys (⟨x,y⟩ :: l) = kinsert x y (erase_dupkeys l) := rfl
id                                                └──┘  └───┘      └───────────┘      └┘    └─────┘    └───────────┘      └─┘
src                                                  └──┘  └───┘       └───────────┘        └┘     └─────┘      └───────────┘       └─┘
typ                                               └──┘  └───┘      └───────────┘      └┘    └─────┘    └───────────┘      └─┘
doc                                                                                                 └─────┘
518  
519  lemma nodupkeys_erase_dupkeys (l : list (sigma β)) : nodupkeys (erase_dupkeys l) :=
id                                      └──┘  └───┘      └───────┘  └───────────┘ 
src                                     └──┘  └───┘       └───────┘  └───────────┘
typ                                     └──┘  └───┘      └───────┘  └───────────┘ 
520  begin
st   └─────
521    dsimp [erase_dupkeys], generalize hl : nil = l',
id            └───────────┘                   └─┘
src    └─────┘└───────────┘  └──────────────┘└─┘ 
typ    └─────┘└───────────┘  └──────────────┘└─┘ 
doc    └─────┘               └──────────────┘    
txt    └─────┘               └──────────────┘    
par    └─────┘               └──────────────┘    
pid                                  └─┘└┘    
st   ──────────────────────┘└────────────────────────┘└─
522    have : nodupkeys l', { rw ← hl, apply nodup_nil },
id            └───────┘ └┘         └┘        └───────┘
src    └─────┘└───────┘      └───┘    └────┘└───────┘
typ    └─────┘└───────┘└┘    └───┘└┘  └────┘└───────┘
doc    └─────┘               └───┘    └────┘         
txt    └─────┘               └───┘    └────┘         
par    └─────┘               └───┘    └────┘         
pid    └───┘└┘                 └─┘                  
st   ────────────────────┘└──┘└─────┘└────────────────┘└┘
523    clear hl,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid         └─┘
st   ─────────┘└─
524    induction l with x xs,
id               
src    └────────┘ └────────┘
typ    └────────┘└────────┘
doc    └────────┘ └────────┘
txt    └────────┘ └────────┘
par    └────────┘ └────────┘
pid              └───────┘
st   ──────────────────────┘└─
525    { apply this },
src      └────┘    
typ      └────┘    
doc      └────┘    
txt      └────┘    
par      └────┘    
pid               
st   ───┘└─────────┘└┘
526    { cases x, simp [erase_dupkeys], split,
id                     └───────────┘
src      └────┘   └────┘└───────────┘  └───┘
typ      └────┘  └────┘└───────────┘  └───┘
doc      └────┘   └────┘               └───┘
txt      └────┘   └────┘               └───┘
par      └────┘   └────┘               └───┘
pid                               
st   ──────────┘└────────────────────┘└─────┘└─
527      { simp [keys_kerase], apply mem_erase_of_nodup l_ih },
id               └─────────┘         └────────────────┘ └──┘
src        └────┘└─────────┘  └────┘└────────────────┘    
typ        └────┘└─────────┘  └────┘└────────────────┘└──┘
doc        └────┘             └────┘                      
txt        └────┘             └────┘                      
par        └────┘             └────┘                      
pid                                                    
st   ─────┘└────────────────┘└──────────────────────────────┘└┘
528      apply kerase_nodupkeys _ l_ih, }
id             └──────────────┘   └──┘
src      └────┘└──────────────┘└─┘
typ      └────┘└──────────────┘└─┘└──┘
doc      └────┘                └─┘
txt      └────┘                └─┘
par      └────┘                └─┘
pid                           └─┘
st   ────────────────────────────────┘└───
529  end
st   ──┘
530  
531  lemma lookup_erase_dupkeys (a : α) (l : list (sigma β)) : lookup a (erase_dupkeys l) = lookup a l :=
id                                          └──┘  └───┘      └────┘   └───────────┘    └────┘  
src                                          └──┘  └───┘       └────┘    └───────────┘     └────┘
typ                                         └──┘  └───┘      └────┘   └───────────┘    └────┘  
doc                                                            └────┘                       └────┘
532  begin
st   └─────
533    induction l, refl,
id               
src    └────────┘   └──┘
typ    └────────┘  └──┘
doc    └────────┘   └──┘
txt    └────────┘   └──┘
par    └────────┘   └──┘
pid             
st   ────────────┘└────┘└─
534    cases l_hd with a' b,
id           └──┘
src    └────┘    └────────┘
typ    └────┘└──┘└────────┘
doc    └────┘    └────────┘
txt    └────┘    └────────┘
par    └────┘    └────────┘
pid             └────────┘
st   ─────────────────────┘└─
535    by_cases a = a',
id                └┘
src    └───────┘ 
typ    └───────┘└┘
doc    └───────┘  
txt    └───────┘  
par    └───────┘  
pid              
st   ────────────────┘└─
536    { subst a', rw [erase_dupkeys_cons,lookup_kinsert,lookup_cons_eq] },
id             └┘      └────────────────┘ └────────────┘ └────────────┘
src      └────┘    └──┘└────────────────┘└────────────┘└────────────┘└┘
typ      └────┘└┘  └──┘└────────────────┘└────────────┘└────────────┘└┘
doc      └────┘    └──┘                                              └┘
txt      └────┘    └──┘                                              └┘
par      └────┘    └──┘                                              └┘
pid                 └┘                                              
st   ───┘└──────┘└──────────────────────┘└─────────────┘└─────────────┘└┘
537    { rw [erase_dupkeys_cons,lookup_kinsert_ne h,l_ih,lookup_cons_ne], exact h },
id           └────────────────┘ └───────────────┘  └──┘ └────────────┘         
src      └──┘└────────────────┘└───────────────┘     └────────────┘  └────┘ 
typ      └──┘└────────────────┘└───────────────┘└──┘└────────────┘  └────┘
doc      └──┘                                                        └────┘ 
txt      └──┘                                                        └────┘ 
par      └──┘                                                        └────┘ 
pid        └┘                                                              
st   ─────────────────────────┘└──────────────────┘└───┘└─────────────┘└─────────┘└──
538  end
st   ──┘
539  
540  /- kunion -/
541  
542  /-- `kunion l₁ l₂` is the append to l₁ of l₂ after, for each key in l₁, the
543  first matching pair in l₂ is erased. -/
544  def kunion : list (sigma β) → list (sigma β) → list (sigma β)
id                └──┘  └───┘    └──┘  └───┘     └──┘  └───┘ 
src               └──┘  └───┘      └──┘  └───┘      └──┘  └───┘
typ               └──┘  └───┘    └──┘  └───┘     └──┘  └───┘ 
545  | []        l₂ := l₂
id     └┘        └┘
src    └┘
typ    └┘        └┘
546  | (s :: l₁) l₂ := s :: kunion l₁ (kerase s.1 l₂)
id       └┘ └┘  └┘      └┘ └────┘     └────┘  
src       └┘             └┘            └────┘  
typ      └┘ └┘  └┘      └┘ └────┘     └────┘  
doc                                    └────┘
547  
548  @[simp] theorem nil_kunion {l : list (sigma β)} : kunion [] l = l :=
id                                   └──┘  └───┘      └────┘ └┘   
src                                  └──┘  └───┘       └────┘ └┘   
typ                                  └──┘  └───┘      └────┘ └┘   
doc    └──┘                                            └────┘
549  rfl
id   └─┘
src  └─┘
typ  └─┘
550  
551  @[simp] theorem kunion_nil : ∀ {l : list (sigma β)}, kunion l [] = l
id                                      └──┘  └───┘     └────┘  └┘  
src                                      └──┘  └───┘      └────┘   └┘ 
typ                                     └──┘  └───┘     └────┘  └┘  
doc    └──┘                                               └────┘
552  | []       := rfl
id     └┘          └─┘
src    └┘          └─┘
typ    └┘          └─┘
553  | (_ :: l) := by rw [kunion, kerase_nil, kunion_nil]
id        └┘              └────┘  └────────┘
src       └┘          └──┘└────┘└┘└────────┘└┘          └─
typ       └┘          └──┘└────┘└┘└────────┘└┘└────────┘└─
doc                   └──┘└────┘└┘          └┘          └─
txt                   └──┘      └┘          └┘          └─
par                   └──┘      └┘          └┘          └─
pid                     └┘      └┘          └┘          
st                   └─────────┘└──────────┘└──────────┘
554  
src  
typ  
doc  
txt  
par  
pid  
st   
555  @[simp] theorem kunion_cons {s} {l₁ l₂ : list (sigma β)} :
id                                            └──┘  └───┘ 
src                                           └──┘  └───┘
typ                                           └──┘  └───┘ 
doc    └──┘
556    kunion (s :: l₁) l₂ = s :: kunion l₁ (kerase s.1 l₂) :=
id     └────┘   └┘ └┘  └┘   └┘ └────┘ └┘  └────┘   └┘
src    └────┘    └┘           └┘ └────┘     └────┘  
typ    └────┘   └┘ └┘  └┘   └┘ └────┘ └┘  └────┘   └┘
doc    └────┘                     └────┘     └────┘
557  rfl
id   └─┘
src  └─┘
typ  └─┘
558  
559  @[simp] theorem mem_keys_kunion {a} {l₁ l₂ : list (sigma β)} :
id                                                └──┘  └───┘ 
src                                               └──┘  └───┘
typ                                               └──┘  └───┘ 
doc    └──┘
560    a ∈ (kunion l₁ l₂).keys ↔ a ∈ l₁.keys ∨ a ∈ l₂.keys :=
id        └────┘ └┘ └┘ └──┘     └┘└───┘    └┘└───┘
src        └────┘       └──┘        └───┘       └───┘
typ       └────┘ └┘ └┘ └──┘     └┘└───┘    └┘└───┘
doc         └────┘       └──┘          └───┘         └───┘
561  begin
st   └─────
562    induction l₁ generalizing l₂,
id               └┘
src    └────────┘  └──────────────┘
typ    └────────┘└┘└──────────────┘
doc    └────────┘  └──────────────┘
txt    └────────┘  └──────────────┘
par    └────────┘  └──────────────┘
pid               └─────────────┘
st   ─────────────────────────────┘└─
563    case list.nil { simp },
src    └──────────────┘└───┘
typ    └──────────────┘└───┘
doc    └──────────────┘└───┘
txt    └──────────────┘└───┘
par    └──────────────┘└───┘
pid        └───────┘└──────┘
st   ────────────────┘└────┘└┘
564    case list.cons : s l₁ ih { by_cases h : a = s.1; [simp [h], simp [h, ih]] }
id                                                                   
src    └─────────────────────────┘└───────┘ └─┘  └┘└─┘└────┘ └┘└────┘ └┘  └──┘
typ    └─────────────────────────┘└───────┘ └─┘└┘└─┘└────┘└┘└────┘└┘└┘└──┘
doc    └─────────────────────────┘└───────┘ └─┘   └┘└─┘└────┘ └┘└────┘ └┘  └──┘
txt    └─────────────────────────┘└───────┘ └─┘   └┘└─┘└────┘ └┘└────┘ └┘  └──┘
par    └─────────────────────────┘└───────┘ └─┘   └┘└─┘└────┘ └┘└────┘ └┘  └──┘
pid        └────────┘└────────┘└──────────┘ └─┘   └─────────┘ └───────┘ └┘  └──┘
st   ───────────────────────────┘└─────────────────────────────────────────────┘└┘
565  end
st   └─┘
566  
567  @[simp] theorem kunion_kerase {a} : ∀ {l₁ l₂ : list (sigma β)},
id                                                 └──┘  └───┘ 
src                                                 └──┘  └───┘
typ                                                └──┘  └───┘ 
doc    └──┘
568    kunion (kerase a l₁) (kerase a l₂) = kerase a (kunion l₁ l₂)
id     └────┘  └────┘  └┘   └────┘  └┘   └────┘   └────┘ └┘ └┘
src    └────┘  └────┘        └────┘        └────┘    └────┘
typ    └────┘  └────┘  └┘   └────┘  └┘   └────┘   └────┘ └┘ └┘
doc    └────┘  └────┘        └────┘         └────┘    └────┘
569  | []       _ := rfl
id     └┘            └─┘
src    └┘            └─┘
typ    └┘            └─┘
570  | (s :: _) l := by by_cases h : a = s.1;
id        └┘                           
src       └┘            └───────┘ └─┘  └┘
typ       └┘            └───────┘ └─┘└┘
doc                     └───────┘ └─┘   └┘
txt                     └───────┘ └─┘   └┘
par                     └───────┘ └─┘   └┘
pid                              └─┘   └┘
st                     └──────────────────────
571                     simp [h, kerase_comm a s.1 l, kunion_kerase]
id                              └─────────┘     
src                     └────┘ └┘└─────────┘  └─┘ └┘             └─
typ                     └────┘└┘└─────────┘└─┘└┘└───────────┘└─
doc                     └────┘ └┘             └─┘ └┘             └─
txt                     └────┘ └┘             └─┘ └┘             └─
par                     └────┘ └┘             └─┘ └┘             └─
pid                          └┘             └─┘ └┘             
st   ────────────────────────────────────────────────────────────────
572  
src  
typ  
doc  
txt  
par  
pid  
st   
573  theorem kunion_nodupkeys {l₁ l₂ : list (sigma β)}
id                                     └──┘  └───┘ 
src                                    └──┘  └───┘
typ                                    └──┘  └───┘ 
574    (nd₁ : l₁.nodupkeys) (nd₂ : l₂.nodupkeys) : (kunion l₁ l₂).nodupkeys :=
id            └┘└────────┘         └┘└────────┘     └────┘ └┘ └┘ └───────┘
src             └────────┘           └────────┘     └────┘       └───────┘
typ           └┘└────────┘         └┘└────────┘     └────┘ └┘ └┘ └───────┘
doc                                                 └────┘
575  begin
st   └─────
576    induction l₁ generalizing l₂,
id               └┘
src    └────────┘  └──────────────┘
typ    └────────┘└┘└──────────────┘
doc    └────────┘  └──────────────┘
txt    └────────┘  └──────────────┘
par    └────────┘  └──────────────┘
pid               └─────────────┘
st   ─────────────────────────────┘└─
577    case list.nil { simp only [nil_kunion, nd₂] },
id                                └────────┘  └─┘
src    └──────────────┘└─────────┘└────────┘└┘   └┘
typ    └──────────────┘└─────────┘└────────┘└┘└─┘└┘
doc    └──────────────┘└─────────┘          └┘   └┘
txt    └──────────────┘└─────────┘          └┘   └┘
par    └──────────────┘└─────────┘          └┘   └┘
pid        └───────┘└───────────┘          └┘   └─┘
st   ────────────────┘└───────────────────────────┘└┘
578    case list.cons : s l₁ ih {
src    └──────────────────────────
typ    └──────────────────────────
doc    └──────────────────────────
txt    └──────────────────────────
par    └──────────────────────────
pid        └────────┘└────────┘└──
st   ───────────────────────────┘
579      simp at nd₁,
src  ───┘└─────────┘└─
typ  ───┘└─────────┘└─
doc  ───┘└─────────┘└─
txt  ───┘└─────────┘└─
par  ───┘└─────────┘└─
pid  ─────────────────
st   ──────────────┘└─
580      simp [not_or_distrib, nd₁.1, nd₂, ih nd₁.2 (kerase_nodupkeys s.1 nd₂)] }
id             └────────────┘  └─┘    └─┘  └┘ └─┘    └──────────────┘    └─┘
src  ───┘└────┘└────────────┘└┘   └──┘   └┘     └─┘ └──────────────┘ └─┘   └─┘└┘
typ  ───┘└────┘└────────────┘└┘└─┘└──┘└─┘└┘└┘└─┘└─┘ └──────────────┘└─┘└─┘└─┘└┘
doc  ───┘└────┘              └┘   └──┘   └┘     └─┘                  └─┘   └─┘└┘
txt  ───┘└────┘              └┘   └──┘   └┘     └─┘                  └─┘   └─┘└┘
par  ───┘└────┘              └┘   └──┘   └┘     └─┘                  └─┘   └─┘└┘
pid  ─────────┘              └┘   └──┘   └┘     └─┘                  └─┘   └──┘
st   ──────────────────────────────────────────────────────────────────────────┘
581  end
st   └─┘
582  
583  theorem perm_kunion_left {l₁ l₂ : list (sigma β)} (p : l₁ ~ l₂) (l) :
id                                     └──┘  └───┘         └┘  └┘
src                                    └──┘  └───┘             
typ                                    └──┘  └───┘         └┘  └┘
doc                                                            
584    kunion l₁ l ~ kunion l₂ l :=
id     └────┘ └┘   └────┘ └┘ 
src    └────┘       └────┘
typ    └────┘ └┘   └────┘ └┘ 
doc    └────┘       └────┘
585  begin
st   └─────
586    induction p generalizing l,
id               
src    └────────┘ └─────────────┘
typ    └────────┘└─────────────┘
doc    └────────┘ └─────────────┘
txt    └────────┘ └─────────────┘
par    └────────┘ └─────────────┘
pid              └────────────┘
st   ───────────────────────────┘└─
587    case list.perm.nil { refl },
src    └───────────────────┘└───┘
typ    └───────────────────┘└───┘
doc    └───────────────────┘└───┘
txt    └───────────────────┘└───┘
par    └───────────────────┘└───┘
pid        └────────────┘└──────┘
st   ─────────────────────┘└────┘└┘
588    case list.perm.skip : hd tl₁ tl₂ p ih {
src    └───────────────────────────────────────
typ    └───────────────────────────────────────
doc    └───────────────────────────────────────
txt    └───────────────────────────────────────
par    └───────────────────────────────────────
pid        └─────────────┘└────────────────┘└──
st   ────────────────────────────────────────┘
589      simp [ih (kerase hd.1 l), perm.skip] },
id             └┘  └────┘ └┘      └───────┘
src  ───┘└────┘   └────┘  └─┘ └─┘└───────┘└┘
typ  ───┘└────┘└┘ └────┘└┘└─┘└─┘└───────┘└┘
doc  ───┘└────┘   └────┘  └─┘ └─┘         └┘
txt  ───┘└────┘           └─┘ └─┘         └┘
par  ───┘└────┘           └─┘ └─┘         └┘
pid  ─────────┘           └─┘ └─┘         └─┘
st   ────────────────────────────────────────┘└┘
590    case list.perm.swap : s₁ s₂ l {
src    └───────────────────────────────
typ    └───────────────────────────────
doc    └───────────────────────────────
txt    └───────────────────────────────
par    └───────────────────────────────
pid        └─────────────┘└────────┘└──
st   ────────────────────────────────┘
591      simp [kerase_comm, perm.swap] },
id             └─────────┘  └───────┘
src  ───┘└────┘└─────────┘└┘└───────┘└┘
typ  ───┘└────┘└─────────┘└┘└───────┘└┘
doc  ───┘└────┘           └┘         └┘
txt  ───┘└────┘           └┘         └┘
par  ───┘└────┘           └┘         └┘
pid  ─────────┘           └┘         └─┘
st   ─────────────────────────────────┘└┘
592    case list.perm.trans : l₁ l₂ l₃ p₁₂ p₂₃ ih₁₂ ih₂₃ {
src    └───────────────────────────────────────────────────
typ    └───────────────────────────────────────────────────
doc    └───────────────────────────────────────────────────
txt    └───────────────────────────────────────────────────
par    └───────────────────────────────────────────────────
pid        └──────────────┘└───────────────────────────┘└──
st   ────────────────────────────────────────────────────┘
593      exact perm.trans (ih₁₂ l) (ih₂₃ l) }
id             └────────┘  └──┘     └──┘ 
src  ───┘└────┘└────────┘      └┘      └┘└┘
typ  ───┘└────┘└────────┘ └──┘ └┘ └──┘└┘└┘
doc  ───┘└────┘                └┘      └┘└┘
txt  ───┘└────┘                └┘      └┘└┘
par  ───┘└────┘                └┘      └┘└┘
pid  ─────────┘                └┘      └─┘
st   ──────────────────────────────────────┘
594  end
st   └─┘
595  
596  theorem perm_kunion_right : ∀ l {l₁ l₂ : list (sigma β)},
id                                           └──┘  └───┘ 
src                                           └──┘  └───┘
typ                                          └──┘  └───┘ 
597    l₁.nodupkeys → l₁ ~ l₂ → kunion l l₁ ~ kunion l l₂
id     └┘└────────┘   └┘  └┘   └────┘  └┘  └────┘  └┘
src      └────────┘            └────┘       └────┘
typ    └┘└────────┘   └┘  └┘   └────┘  └┘  └────┘  └┘
doc                            └────┘       └────┘
598  | []       _  _  _   p := p
id     └┘                 
src    └┘
typ    └┘                 
599  | (s :: l) l₁ l₂ nd₁ p :=
id        └┘
src       └┘
typ       └┘
600    by simp [perm.skip s
id              └───────┘
src       └────┘└───────┘ 
typ       └────┘└───────┘ 
doc       └────┘          
txt       └────┘          
par       └────┘          
pid                     
st       └──────────────────
601      (perm_kunion_right l (kerase_nodupkeys s.1 nd₁) (perm_kerase nd₁ p))]
id        └───────────────┘   └──────────────┘          └─────────┘ └─┘ 
src  ───┘                    └──────────────┘ └─┘   └┘ └─────────┘    └───
typ  ───┘ └───────────────┘ └──────────────┘└─┘   └┘ └─────────┘└─┘└───
doc  ───┘                                     └─┘   └┘                └───
txt  ───┘                                     └─┘   └┘                └───
par  ───┘                                     └─┘   └┘                └───
pid  ───┘                                     └─┘   └┘                └─┘
st   ──────────────────────────────────────────────────────────────────────────
602  
src  
typ  
doc  
txt  
par  
pid  
st   
603  theorem perm_kunion {l₁ l₂ l₃ l₄ : list (sigma β)} (nd₃ : l₃.nodupkeys)
id                                      └──┘  └───┘           └┘└────────┘
src                                     └──┘  └───┘              └────────┘
typ                                     └──┘  └───┘           └┘└────────┘
604    (p₁₂ : l₁ ~ l₂) (p₃₄ : l₃ ~ l₄) : kunion l₁ l₃ ~ kunion l₂ l₄ :=
id            └┘  └┘         └┘  └┘    └────┘ └┘ └┘  └────┘ └┘ └┘
src                                    └────┘        └────┘
typ           └┘  └┘         └┘  └┘    └────┘ └┘ └┘  └────┘ └┘ └┘
doc                                    └────┘        └────┘
605  perm.trans (perm_kunion_left p₁₂ l₃) (perm_kunion_right l₂ nd₃ p₃₄)
id   └────────┘  └──────────────┘ └─┘ └┘   └───────────────┘ └┘ └─┘ └─┘
src  └────────┘  └──────────────┘          └───────────────┘
typ  └────────┘  └──────────────┘ └─┘ └┘   └───────────────┘ └┘ └─┘ └─┘
606  
607  @[simp] theorem lookup_kunion_left {a} {l₁ l₂ : list (sigma β)} (h : a ∈ l₁.keys) :
id                                                   └──┘  └───┘           └┘└───┘
src                                                  └──┘  └───┘               └───┘
typ                                                  └──┘  └───┘           └┘└───┘
doc    └──┘                                                                     └───┘
608    lookup a (kunion l₁ l₂) = lookup a l₁ :=
id     └────┘   └────┘ └┘ └┘   └────┘  └┘
src    └────┘    └────┘         └────┘
typ    └────┘   └────┘ └┘ └┘   └────┘  └┘
doc    └────┘    └────┘          └────┘
609  begin
st   └─────
610    induction l₁ with s _ ih generalizing l₂; simp at h; cases h; cases s with a',
id               └┘                                                       
src    └────────┘  └──────────────────────────┘  └───────┘  └────┘   └────┘ └──────┘
typ    └────────┘└┘└──────────────────────────┘  └───────┘  └────┘  └────┘└──────┘
doc    └────────┘  └──────────────────────────┘  └───────┘  └────┘   └────┘ └──────┘
txt    └────────┘  └──────────────────────────┘  └───────┘  └────┘   └────┘ └──────┘
par    └────────┘  └──────────────────────────┘  └───────┘  └────┘   └────┘ └──────┘
pid               └─────────┘└──────────────┘      └──┘                └──────┘
st   ──────────────────────────────────────────────────────────────────────────────┘└─
611    { subst h, simp },
id             
src      └────┘   └───┘
typ      └────┘  └───┘
doc      └────┘   └───┘
txt      └────┘   └───┘
par      └────┘   └───┘
pid                  
st   ───┘└─────┘└─────┘└┘
612    { rw kunion_cons,
id          └─────────┘
src      └─┘└─────────┘
typ      └─┘└─────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ─────────────────┘└─
613      by_cases h' : a = a',
id                       └┘
src      └───────┘  └─┘ 
typ      └───────┘  └─┘└┘
doc      └───────┘  └─┘  
txt      └───────┘  └─┘  
par      └───────┘  └─┘  
pid                └─┘  
st   ───────────────────────┘└─
614      { subst h', simp },
id               └┘
src        └────┘    └───┘
typ        └────┘└┘  └───┘
doc        └────┘    └───┘
txt        └────┘    └───┘
par        └────┘    └───┘
pid                     
st   ─────┘└──────┘└─────┘└┘
615      { simp [h', ih h] } }
id               └┘  └┘ 
src        └────┘  └┘   └┘
typ        └────┘└┘└┘└┘└┘
doc        └────┘  └┘   └┘
txt        └────┘  └┘   └┘
par        └────┘  └┘   └┘
pid              └┘   
st   ─────────────────────┘└───
616  end
st   ──┘
617  
618  @[simp] theorem lookup_kunion_right {a} {l₁ l₂ : list (sigma β)} (h : a ∉ l₁.keys) :
id                                                    └──┘  └───┘           └┘└───┘
src                                                   └──┘  └───┘               └───┘
typ                                                   └──┘  └───┘           └┘└───┘
doc    └──┘                                                                      └───┘
619    lookup a (kunion l₁ l₂) = lookup a l₂ :=
id     └────┘   └────┘ └┘ └┘   └────┘  └┘
src    └────┘    └────┘         └────┘
typ    └────┘   └────┘ └┘ └┘   └────┘  └┘
doc    └────┘    └────┘          └────┘
620  begin
st   └─────
621    induction l₁ generalizing l₂,
id               └┘
src    └────────┘  └──────────────┘
typ    └────────┘└┘└──────────────┘
doc    └────────┘  └──────────────┘
txt    └────────┘  └──────────────┘
par    └────────┘  └──────────────┘
pid               └─────────────┘
st   ─────────────────────────────┘└─
622    case list.nil { simp },
src    └──────────────┘└───┘
typ    └──────────────┘└───┘
doc    └──────────────┘└───┘
txt    └──────────────┘└───┘
par    └──────────────┘└───┘
pid        └───────┘└──────┘
st   ────────────────┘└────┘└┘
623    case list.cons : _ _ ih { simp [not_or_distrib] at h, simp [h.1, ih h.2] }
id                                     └────────────┘                  └┘ 
src    └────────────────────────┘└────┘└────────────┘└────┘└┘└────┘ └──┘   └──┘└┘
typ    └────────────────────────┘└────┘└────────────┘└────┘└┘└────┘└──┘└┘└──┘└┘
doc    └────────────────────────┘└────┘              └────┘└┘└────┘ └──┘   └──┘└┘
txt    └────────────────────────┘└────┘              └────┘└┘└────┘ └──┘   └──┘└┘
par    └────────────────────────┘└────┘              └────┘└┘└────┘ └──┘   └──┘└┘
pid        └────────┘└───────┘└───────┘              └────────────┘ └──┘   └───┘
st   ──────────────────────────┘└─────────────────────────┘└───────────────────┘
624  end
st   └─┘
625  
626  @[simp] theorem mem_lookup_kunion {a} {b : β a} {l₁ l₂ : list (sigma β)} :
id                                                          └──┘  └───┘ 
src                                                           └──┘  └───┘
typ                                                         └──┘  └───┘ 
doc    └──┘
627    b ∈ lookup a (kunion l₁ l₂) ↔ b ∈ lookup a l₁ ∨ a ∉ l₁.keys ∧ b ∈ lookup a l₂ :=
id       └────┘   └────┘ └┘ └┘     └────┘  └┘    └┘└───┘    └────┘  └┘
src       └────┘    └────┘            └────┘            └───┘     └────┘
typ      └────┘   └────┘ └┘ └┘     └────┘  └┘    └┘└───┘    └────┘  └┘
doc        └────┘    └────┘              └────┘              └───┘       └────┘
628  begin
st   └─────
629    induction l₁ generalizing l₂,
id               └┘
src    └────────┘  └──────────────┘
typ    └────────┘└┘└──────────────┘
doc    └────────┘  └──────────────┘
txt    └────────┘  └──────────────┘
par    └────────┘  └──────────────┘
pid               └─────────────┘
st   ─────────────────────────────┘└─
630    case list.nil { simp },
src    └──────────────┘└───┘
typ    └──────────────┘└───┘
doc    └──────────────┘└───┘
txt    └──────────────┘└───┘
par    └──────────────┘└───┘
pid        └───────┘└──────┘
st   ────────────────┘└────┘└┘
631    case list.cons : s _ ih {
src    └─────────────────────────
typ    └─────────────────────────
doc    └─────────────────────────
txt    └─────────────────────────
par    └─────────────────────────
pid        └────────┘└───────┘└──
st   ──────────────────────────┘
632      cases s with a',
id             
src  ───┘└────┘ └──────┘└─
typ  ───┘└────┘└──────┘└─
doc  ───┘└────┘ └──────┘└─
txt  ───┘└────┘ └──────┘└─
par  ───┘└────┘ └──────┘└─
pid  ─────────┘ └─────────
st   ──────────────────┘└─
633      by_cases h₁ : a = a',
id                       └┘
src  ───┘└───────┘  └─┘   └─
typ  ───┘└───────┘  └─┘└┘└─
doc  ───┘└───────┘  └─┘    └─
txt  ───┘└───────┘  └─┘    └─
par  ───┘└───────┘  └─┘    └─
pid  ────────────┘  └─┘    └─
st   ───────────────────────┘└─
634      { subst h₁, simp },
id               └┘
src  ─────┘└────┘  └┘└───┘└──
typ  ─────┘└────┘└┘└┘└───┘└──
doc  ─────┘└────┘  └┘└───┘└──
txt  ─────┘└────┘  └┘└───┘└──
par  ─────┘└────┘  └┘└───┘└──
pid  ───────────┘  └─────────
st   ────┘└───────┘└─────┘└─
635      { let h₂ := @ih (kerase a' l₂), simp [h₁] at h₂, simp [h₁, h₂] } }
id                    └┘  └────┘ └┘ └┘         └┘               └┘  └┘
src  ─────┘└────────┘    └────┘    └┘└────┘  └─────┘└┘└────┘  └┘  └┘└──┘
typ  ─────┘└────────┘ └┘ └────┘└┘└┘└┘└────┘└┘└─────┘└┘└────┘└┘└┘└┘└┘└──┘
doc  ─────┘└────────┘    └────┘    └┘└────┘  └─────┘└┘└────┘  └┘  └┘└──┘
txt  ─────┘└────────┘              └┘└────┘  └─────┘└┘└────┘  └┘  └┘└──┘
par  ─────┘└────────┘              └┘└────┘  └─────┘└┘└────┘  └┘  └┘└──┘
pid  ───────────────┘              └───────┘  └─────────────┘  └┘  └───┘
st   ─────────────────────────────────┘└───────────────┘└──────────────┘└─┘
636  end
st   └─┘
637  
638  theorem mem_lookup_kunion_middle {a} {b : β a} {l₁ l₂ l₃ : list (sigma β)}
id                                                            └──┘  └───┘ 
src                                                             └──┘  └───┘
typ                                                           └──┘  └───┘ 
639    (h₁ : b ∈ lookup a (kunion l₁ l₃)) (h₂ : a ∉ keys l₂) :
id             └────┘   └────┘ └┘ └┘           └──┘ └┘
src             └────┘    └────┘                  └──┘
typ            └────┘   └────┘ └┘ └┘           └──┘ └┘
doc              └────┘    └────┘                   └──┘
640    b ∈ lookup a (kunion (kunion l₁ l₂) l₃) :=
id       └────┘   └────┘  └────┘ └┘ └┘  └┘
src       └────┘    └────┘  └────┘
typ      └────┘   └────┘  └────┘ └┘ └┘  └┘
doc        └────┘    └────┘  └────┘
641  match mem_lookup_kunion.mp h₁ with
id         └───────────────┘└─┘ └┘
src        └───────────────┘└─┘
typ        └───────────────┘└─┘ └┘
642  | or.inl h := mem_lookup_kunion.mpr (or.inl (mem_lookup_kunion.mpr (or.inl h)))
id     └────┘     └───────────────┘└──┘  └────┘  └───────────────┘└──┘  └────┘
src    └────┘      └───────────────┘└──┘  └────┘  └───────────────┘└──┘  └────┘
typ    └────┘     └───────────────┘└──┘  └────┘  └───────────────┘└──┘  └────┘
643  | or.inr h := mem_lookup_kunion.mpr $
id     └────┘     └───────────────┘└──┘
src    └────┘      └───────────────┘└──┘
typ    └────┘     └───────────────┘└──┘
644    or.inr ⟨mt mem_keys_kunion.mp (not_or_distrib.mpr ⟨h.1, h₂⟩), h.2⟩
id     └────┘  └┘ └─────────────┘└─┘  └────────────┘└──┘      └┘     
src    └────┘  └┘ └─────────────┘└─┘  └────────────┘└──┘             
typ    └────┘  └┘ └─────────────┘└─┘  └────────────┘└──┘      └┘     
645  end
646  
647  end list